YES 20.981
H-Termination proof of /home/matraf/haskell/eval_FullyBlown_Fast/List.hs
H-Termination of the given Haskell-Program with start terms could successfully be proven:
↳ HASKELL
↳ CR
mainModule List
| ((insert :: Ratio Int -> [Ratio Int] -> [Ratio Int]) :: Ratio Int -> [Ratio Int] -> [Ratio Int]) |
module List where
| import qualified Maybe import qualified Prelude
|
| insert :: Ord a => a -> [a] -> [a]
insert | e ls | = | insertBy compare e ls |
|
| insertBy :: (a -> a -> Ordering) -> a -> [a] -> [a]
insertBy | _ x [] | = | x : [] |
insertBy | cmp x ys@(y : ys') | = |
case | cmp x y of |
| GT | -> | y : insertBy cmp x ys' |
| _ | -> | x : ys |
|
|
module Maybe where
| import qualified List import qualified Prelude
|
Case Reductions:
The following Case expression
case | cmp x y of |
| GT | → y : insertBy cmp x ys' |
| _ | → x : ys |
is transformed to
insertBy0 | y cmp x ys' ys GT | = y : insertBy cmp x ys' |
insertBy0 | y cmp x ys' ys _ | = x : ys |
↳ HASKELL
↳ CR
↳ HASKELL
↳ BR
mainModule List
| ((insert :: Ratio Int -> [Ratio Int] -> [Ratio Int]) :: Ratio Int -> [Ratio Int] -> [Ratio Int]) |
module List where
| import qualified Maybe import qualified Prelude
|
| insert :: Ord a => a -> [a] -> [a]
insert | e ls | = | insertBy compare e ls |
|
| insertBy :: (a -> a -> Ordering) -> a -> [a] -> [a]
insertBy | _ x [] | = | x : [] |
insertBy | cmp x ys@(y : ys') | = | insertBy0 y cmp x ys' ys (cmp x y) |
|
|
insertBy0 | y cmp x ys' ys GT | = | y : insertBy cmp x ys' |
insertBy0 | y cmp x ys' ys _ | = | x : ys |
|
module Maybe where
| import qualified List import qualified Prelude
|
Replaced joker patterns by fresh variables and removed binding patterns.
Binding Reductions:
The bind variable of the following binding Pattern
ys@(vy : vz)
is replaced by the following term
vy : vz
↳ HASKELL
↳ CR
↳ HASKELL
↳ BR
↳ HASKELL
↳ COR
mainModule List
| ((insert :: Ratio Int -> [Ratio Int] -> [Ratio Int]) :: Ratio Int -> [Ratio Int] -> [Ratio Int]) |
module List where
| import qualified Maybe import qualified Prelude
|
| insert :: Ord a => a -> [a] -> [a]
insert | e ls | = | insertBy compare e ls |
|
| insertBy :: (a -> a -> Ordering) -> a -> [a] -> [a]
insertBy | vx x [] | = | x : [] |
insertBy | cmp x (vy : vz) | = | insertBy0 vy cmp x vz (vy : vz) (cmp x vy) |
|
|
insertBy0 | y cmp x ys' ys GT | = | y : insertBy cmp x ys' |
insertBy0 | y cmp x ys' ys vw | = | x : ys |
|
module Maybe where
| import qualified List import qualified Prelude
|
Cond Reductions:
The following Function with conditions
is transformed to
undefined0 | True | = undefined |
undefined1 | | = undefined0 False |
↳ HASKELL
↳ CR
↳ HASKELL
↳ BR
↳ HASKELL
↳ COR
↳ HASKELL
↳ Narrow
mainModule List
| (insert :: Ratio Int -> [Ratio Int] -> [Ratio Int]) |
module List where
| import qualified Maybe import qualified Prelude
|
| insert :: Ord a => a -> [a] -> [a]
insert | e ls | = | insertBy compare e ls |
|
| insertBy :: (a -> a -> Ordering) -> a -> [a] -> [a]
insertBy | vx x [] | = | x : [] |
insertBy | cmp x (vy : vz) | = | insertBy0 vy cmp x vz (vy : vz) (cmp x vy) |
|
|
insertBy0 | y cmp x ys' ys GT | = | y : insertBy cmp x ys' |
insertBy0 | y cmp x ys' ys vw | = | x : ys |
|
module Maybe where
| import qualified List import qualified Prelude
|
Haskell To QDPs
↳ HASKELL
↳ CR
↳ HASKELL
↳ BR
↳ HASKELL
↳ COR
↳ HASKELL
↳ Narrow
↳ AND
↳ QDP
↳ QDPSizeChangeProof
↳ QDP
↳ QDP
↳ QDP
↳ QDP
Q DP problem:
The TRS P consists of the following rules:
new_primCmpNat(Succ(ww41900), Succ(ww42300)) → new_primCmpNat(ww41900, ww42300)
R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem. From the DPs we obtained the following set of size-change graphs:
- new_primCmpNat(Succ(ww41900), Succ(ww42300)) → new_primCmpNat(ww41900, ww42300)
The graph contains the following edges 1 > 1, 2 > 2
↳ HASKELL
↳ CR
↳ HASKELL
↳ BR
↳ HASKELL
↳ COR
↳ HASKELL
↳ Narrow
↳ AND
↳ QDP
↳ QDP
↳ QDPSizeChangeProof
↳ QDP
↳ QDP
↳ QDP
Q DP problem:
The TRS P consists of the following rules:
new_primPlusNat(Succ(ww5900), Succ(ww401000)) → new_primPlusNat(ww5900, ww401000)
R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem. From the DPs we obtained the following set of size-change graphs:
- new_primPlusNat(Succ(ww5900), Succ(ww401000)) → new_primPlusNat(ww5900, ww401000)
The graph contains the following edges 1 > 1, 2 > 2
↳ HASKELL
↳ CR
↳ HASKELL
↳ BR
↳ HASKELL
↳ COR
↳ HASKELL
↳ Narrow
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDPSizeChangeProof
↳ QDP
↳ QDP
Q DP problem:
The TRS P consists of the following rules:
new_primMulNat(Succ(ww16000), Succ(ww17100)) → new_primMulNat(ww16000, Succ(ww17100))
R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem. From the DPs we obtained the following set of size-change graphs:
- new_primMulNat(Succ(ww16000), Succ(ww17100)) → new_primMulNat(ww16000, Succ(ww17100))
The graph contains the following edges 1 > 1, 2 >= 2
↳ HASKELL
↳ CR
↳ HASKELL
↳ BR
↳ HASKELL
↳ COR
↳ HASKELL
↳ Narrow
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDPSizeChangeProof
↳ QDP
Q DP problem:
The TRS P consists of the following rules:
new_primMulNat0(Succ(ww30000), ww40100) → new_primMulNat0(ww30000, ww40100)
R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem. From the DPs we obtained the following set of size-change graphs:
- new_primMulNat0(Succ(ww30000), ww40100) → new_primMulNat0(ww30000, ww40100)
The graph contains the following edges 1 > 1, 2 >= 2
↳ HASKELL
↳ CR
↳ HASKELL
↳ BR
↳ HASKELL
↳ COR
↳ HASKELL
↳ Narrow
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ DependencyGraphProof
Q DP problem:
The TRS P consists of the following rules:
new_insertBy067(ww4300, ww44, ww45, ww4600, ww47, Succ(ww2600)) → new_insertBy(:%(Neg(Succ(ww45)), Neg(Succ(ww4600))), ww47)
new_insertBy(:%(Pos(Zero), Neg(Succ(ww3100))), :(:%(Pos(Succ(Succ(Zero))), Neg(Zero)), ww41)) → new_insertBy028(ww3100, ww41, new_primPlusNat0(new_primPlusNat0(Zero, Succ(ww3100)), Succ(ww3100)))
new_insertBy077(ww4900, ww50, ww51, ww5200, ww53, Succ(ww31800), Succ(ww35700)) → new_insertBy077(ww4900, ww50, ww51, ww5200, ww53, ww31800, ww35700)
new_insertBy073(ww4900, ww50, ww51, ww5200, ww53, Succ(ww31800), Succ(Zero)) → new_insertBy078(ww4900, ww50, ww51, ww5200, ww53)
new_insertBy(:%(Neg(Zero), Neg(Succ(ww3100))), :(:%(Pos(Succ(Zero)), Pos(Zero)), ww41)) → new_insertBy(:%(Neg(Zero), Neg(Succ(ww3100))), ww41)
new_insertBy(:%(Neg(Succ(ww3000)), Neg(Succ(ww3100))), :(:%(Pos(Succ(Succ(Succ(ww4000000)))), Neg(Zero)), ww41)) → new_insertBy045(ww4000000, ww3000, ww3100, ww41, new_primPlusNat0(new_primPlusNat0(new_primPlusNat0(new_primMulNat1(ww4000000, ww3100), Succ(ww3100)), Succ(ww3100)), Succ(ww3100)))
new_insertBy044(Neg(Succ(ww4900)), ww50, ww51, Pos(Succ(ww5200)), ww53, Zero) → new_insertBy076(ww4900, ww50, ww51, ww5200, ww53, new_primPlusNat0(new_primMulNat1(ww4900, ww5200), Succ(ww5200)))
new_insertBy048(ww3000, ww3100, ww41, Succ(ww3410)) → new_insertBy(:%(Neg(Succ(ww3000)), Pos(Succ(ww3100))), ww41)
new_insertBy(:%(Pos(Succ(ww3000)), Neg(Succ(ww3100))), :(:%(Pos(Succ(Zero)), Pos(Zero)), ww41)) → new_insertBy(:%(Pos(Succ(ww3000)), Neg(Succ(ww3100))), ww41)
new_insertBy074(ww4900, ww50, ww51, ww5200, ww53, Succ(ww31800), Succ(Zero)) → new_insertBy082(ww4900, ww50, ww51, ww5200, ww53)
new_insertBy074(ww4900, ww50, ww51, ww5200, ww53, Succ(ww31800), Succ(Succ(ww35900))) → new_insertBy081(ww4900, ww50, ww51, ww5200, ww53, ww31800, ww35900)
new_insertBy(:%(Pos(Succ(ww3000)), Pos(Succ(ww3100))), :(:%(Neg(Succ(Succ(Zero))), Neg(Zero)), ww41)) → new_insertBy022(ww3000, ww3100, ww41, new_primPlusNat0(new_primPlusNat0(Zero, Succ(ww3100)), Succ(ww3100)))
new_insertBy037(ww40100, ww3100, ww41, Succ(ww2800)) → new_insertBy(:%(Neg(Zero), Neg(Succ(ww3100))), ww41)
new_insertBy(:%(Neg(Zero), Neg(Succ(ww3100))), :(:%(Pos(Succ(Succ(Zero))), Pos(Succ(ww40100))), ww41)) → new_insertBy037(ww40100, ww3100, ww41, new_primPlusNat0(new_primPlusNat0(Zero, Succ(ww3100)), Succ(ww3100)))
new_insertBy049(ww4000000, ww40100, ww3100, ww41, Succ(ww3670)) → new_insertBy(:%(Neg(Zero), Neg(Succ(ww3100))), ww41)
new_insertBy(:%(Neg(Succ(ww3000)), Pos(Succ(ww3100))), :(:%(Neg(Succ(Succ(Zero))), Pos(Zero)), ww41)) → new_insertBy035(ww3000, ww3100, ww41, new_primPlusNat0(new_primPlusNat0(Zero, Succ(ww3100)), Succ(ww3100)))
new_insertBy046(ww3000, ww3100, ww41, Succ(ww3350)) → new_insertBy(:%(Neg(Succ(ww3000)), Neg(Succ(ww3100))), ww41)
new_insertBy038(ww4000000, ww40100, ww3100, ww41, Succ(ww2820)) → new_insertBy(:%(Neg(Zero), Pos(Succ(ww3100))), ww41)
new_insertBy(:%(Neg(Succ(ww3000)), Neg(Succ(ww3100))), :(:%(Pos(Succ(Succ(Zero))), Pos(Zero)), ww41)) → new_insertBy033(ww3000, ww3100, ww41, new_primPlusNat0(new_primPlusNat0(Zero, Succ(ww3100)), Succ(ww3100)))
new_insertBy069(ww4300, ww44, ww45, ww4600, ww47, Succ(ww26600), Succ(ww22900)) → new_insertBy069(ww4300, ww44, ww45, ww4600, ww47, ww26600, ww22900)
new_insertBy07(ww3000, ww3100, ww41, Succ(ww700)) → new_insertBy(:%(Pos(Succ(ww3000)), Neg(Succ(ww3100))), ww41)
new_insertBy014(ww4000000, ww3100, ww41, Succ(ww1260)) → new_insertBy(:%(Pos(Zero), Neg(Succ(ww3100))), ww41)
new_insertBy(:%(Neg(Zero), Neg(Succ(ww3100))), :(:%(Pos(Succ(Succ(Succ(ww4000000)))), Pos(Zero)), ww41)) → new_insertBy040(ww4000000, ww3100, ww41, new_primPlusNat0(new_primPlusNat0(new_primPlusNat0(new_primMulNat1(ww4000000, ww3100), Succ(ww3100)), Succ(ww3100)), Succ(ww3100)))
new_insertBy00(ww2400, ww25, ww26, ww2700, ww28, Succ(ww6000), Succ(Zero)) → new_insertBy05(ww2400, ww25, ww26, ww2700, ww28)
new_insertBy059(ww3000, ww31, ww32, ww3300, ww34, Succ(ww1770)) → new_insertBy(:%(Pos(Succ(ww32)), Neg(Succ(ww3300))), ww34)
new_insertBy(:%(Neg(Zero), Neg(Succ(ww3100))), :(:%(Pos(Succ(Succ(Succ(ww4000000)))), Neg(Succ(ww40100))), ww41)) → new_insertBy049(ww4000000, ww40100, ww3100, ww41, new_primPlusNat0(new_primPlusNat0(new_primPlusNat0(new_primMulNat1(ww4000000, ww3100), Succ(ww3100)), Succ(ww3100)), Succ(ww3100)))
new_insertBy(:%(Neg(Zero), Neg(Succ(ww3100))), :(:%(Pos(Succ(Zero)), Pos(Succ(ww40100))), ww41)) → new_insertBy(:%(Neg(Zero), Neg(Succ(ww3100))), ww41)
new_insertBy(:%(Neg(Zero), Neg(Succ(ww3100))), :(:%(Pos(Succ(Succ(Succ(ww4000000)))), Pos(Succ(ww40100))), ww41)) → new_insertBy036(ww4000000, ww40100, ww3100, ww41, new_primPlusNat0(new_primPlusNat0(new_primPlusNat0(new_primMulNat1(ww4000000, ww3100), Succ(ww3100)), Succ(ww3100)), Succ(ww3100)))
new_insertBy(:%(Pos(Zero), Neg(Succ(ww3100))), :(:%(Pos(Succ(Succ(Succ(ww4000000)))), Pos(Zero)), ww41)) → new_insertBy014(ww4000000, ww3100, ww41, new_primPlusNat0(new_primPlusNat0(new_primPlusNat0(new_primMulNat1(ww4000000, ww3100), Succ(ww3100)), Succ(ww3100)), Succ(ww3100)))
new_insertBy(:%(Neg(Succ(ww3000)), Pos(Succ(ww3100))), :(:%(Neg(Succ(Succ(Succ(ww4000000)))), Neg(Zero)), ww41)) → new_insertBy047(ww4000000, ww3000, ww3100, ww41, new_primPlusNat0(new_primPlusNat0(new_primPlusNat0(new_primMulNat1(ww4000000, ww3100), Succ(ww3100)), Succ(ww3100)), Succ(ww3100)))
new_insertBy021(ww4000000, ww3000, ww3100, ww41, Succ(ww1630)) → new_insertBy(:%(Pos(Succ(ww3000)), Pos(Succ(ww3100))), ww41)
new_insertBy044(Pos(Zero), ww50, ww51, Pos(Zero), ww53, Succ(ww3180)) → new_insertBy(:%(Neg(Succ(ww51)), Pos(Zero)), ww53)
new_insertBy(:%(Pos(Zero), Pos(Succ(ww3100))), :(:%(Neg(Succ(Zero)), Pos(Zero)), ww41)) → new_insertBy(:%(Pos(Zero), Pos(Succ(ww3100))), ww41)
new_insertBy(:%(Pos(Succ(ww3000)), Pos(Succ(ww3100))), :(:%(Neg(Succ(Succ(Succ(ww4000000)))), Neg(Zero)), ww41)) → new_insertBy021(ww4000000, ww3000, ww3100, ww41, new_primPlusNat0(new_primPlusNat0(new_primPlusNat0(new_primMulNat1(ww4000000, ww3100), Succ(ww3100)), Succ(ww3100)), Succ(ww3100)))
new_insertBy(:%(Neg(Succ(ww3000)), Pos(Succ(ww3100))), :(:%(Neg(Succ(Zero)), Neg(Zero)), ww41)) → new_insertBy(:%(Neg(Succ(ww3000)), Pos(Succ(ww3100))), ww41)
new_insertBy(:%(Neg(Zero), Pos(Succ(ww3100))), :(:%(Neg(Succ(Succ(Zero))), Pos(Zero)), ww41)) → new_insertBy043(ww3100, ww41, new_primPlusNat0(new_primPlusNat0(Zero, Succ(ww3100)), Succ(ww3100)))
new_insertBy083(ww240, ww25, ww26, ww270, ww28) → new_insertBy(:%(Pos(Succ(ww26)), Neg(ww270)), ww28)
new_insertBy069(ww4300, ww44, ww45, ww4600, ww47, Succ(ww26600), Zero) → new_insertBy070(ww4300, ww44, ww45, ww4600, ww47)
new_insertBy02(ww2400, ww25, ww26, ww2700, ww28, Succ(ww860)) → new_insertBy083(Succ(ww2400), ww25, ww26, Succ(ww2700), ww28)
new_insertBy031(Pos(Succ(ww4300)), ww44, ww45, Neg(Succ(ww4600)), ww47, Zero) → new_insertBy067(ww4300, ww44, ww45, ww4600, ww47, new_primPlusNat0(new_primMulNat1(ww4300, ww4600), Succ(ww4600)))
new_insertBy(:%(Neg(Succ(ww3000)), Pos(Succ(ww3100))), :(:%(Neg(Succ(Succ(Zero))), Neg(Zero)), ww41)) → new_insertBy048(ww3000, ww3100, ww41, new_primPlusNat0(new_primPlusNat0(Zero, Succ(ww3100)), Succ(ww3100)))
new_insertBy0(Pos(Succ(ww2400)), ww25, ww26, Pos(Succ(ww2700)), ww28, Succ(ww600)) → new_insertBy00(ww2400, ww25, ww26, ww2700, ww28, ww600, new_primPlusNat0(new_primMulNat1(ww2400, ww2700), Succ(ww2700)))
new_insertBy044(Pos(Succ(ww4900)), ww50, ww51, Neg(Succ(ww5200)), ww53, Zero) → new_insertBy075(ww4900, ww50, ww51, ww5200, ww53, new_primPlusNat0(new_primMulNat1(ww4900, ww5200), Succ(ww5200)))
new_insertBy045(ww4000000, ww3000, ww3100, ww41, Succ(ww3310)) → new_insertBy(:%(Neg(Succ(ww3000)), Neg(Succ(ww3100))), ww41)
new_insertBy010(ww4000000, ww40100, ww3100, ww41, Succ(ww1020)) → new_insertBy(:%(Pos(Zero), Neg(Succ(ww3100))), ww41)
new_insertBy012(ww4000000, ww40100, ww3100, ww41, Succ(ww1080)) → new_insertBy(:%(Pos(Zero), Pos(Succ(ww3100))), ww41)
new_insertBy057(ww3000, ww31, ww32, ww3300, ww34, Succ(Succ(ww18300)), Succ(ww14400)) → new_insertBy061(ww3000, ww31, ww32, ww3300, ww34, ww18300, ww14400)
new_insertBy(:%(Pos(Zero), Pos(Succ(ww3100))), :(:%(Neg(Succ(Succ(Succ(ww4000000)))), Neg(Succ(ww40100))), ww41)) → new_insertBy025(ww4000000, ww40100, ww3100, ww41, new_primPlusNat0(new_primPlusNat0(new_primPlusNat0(new_primMulNat1(ww4000000, ww3100), Succ(ww3100)), Succ(ww3100)), Succ(ww3100)))
new_insertBy035(ww3000, ww3100, ww41, Succ(ww2500)) → new_insertBy(:%(Neg(Succ(ww3000)), Pos(Succ(ww3100))), ww41)
new_insertBy051(ww4000000, ww40100, ww3100, ww41, Succ(ww3730)) → new_insertBy(:%(Neg(Zero), Pos(Succ(ww3100))), ww41)
new_insertBy(:%(Neg(Succ(ww3000)), Neg(Succ(ww3100))), :(:%(Pos(Succ(Succ(Zero))), Neg(Zero)), ww41)) → new_insertBy046(ww3000, ww3100, ww41, new_primPlusNat0(new_primPlusNat0(Zero, Succ(ww3100)), Succ(ww3100)))
new_insertBy016(ww4000000, ww3100, ww41, Succ(ww1320)) → new_insertBy(:%(Pos(Zero), Pos(Succ(ww3100))), ww41)
new_insertBy081(ww4900, ww50, ww51, ww5200, ww53, Succ(ww31800), Succ(ww35900)) → new_insertBy081(ww4900, ww50, ww51, ww5200, ww53, ww31800, ww35900)
new_insertBy0(Neg(Succ(ww2400)), ww25, ww26, Pos(Succ(ww2700)), ww28, Zero) → new_insertBy03(ww2400, ww25, ww26, ww2700, ww28, new_primPlusNat0(new_primMulNat1(ww2400, ww2700), Succ(ww2700)))
new_insertBy(:%(Pos(Zero), Pos(Succ(ww3100))), :(:%(Neg(Succ(Succ(Succ(ww4000000)))), Pos(Succ(ww40100))), ww41)) → new_insertBy012(ww4000000, ww40100, ww3100, ww41, new_primPlusNat0(new_primPlusNat0(new_primPlusNat0(new_primMulNat1(ww4000000, ww3100), Succ(ww3100)), Succ(ww3100)), Succ(ww3100)))
new_insertBy061(ww3000, ww31, ww32, ww3300, ww34, Succ(ww18300), Succ(ww14400)) → new_insertBy061(ww3000, ww31, ww32, ww3300, ww34, ww18300, ww14400)
new_insertBy044(Pos(Zero), ww50, ww51, Pos(Succ(ww5200)), ww53, Succ(ww3180)) → new_insertBy(:%(Neg(Succ(ww51)), Pos(Succ(ww5200))), ww53)
new_insertBy(:%(Neg(Succ(ww3000)), Neg(Succ(ww3100))), :(:%(Pos(Succ(Zero)), Neg(Zero)), ww41)) → new_insertBy(:%(Neg(Succ(ww3000)), Neg(Succ(ww3100))), ww41)
new_insertBy084(ww240, ww25, ww26, ww270, ww28) → new_insertBy(:%(Pos(Succ(ww26)), Pos(ww270)), ww28)
new_insertBy028(ww3100, ww41, Succ(ww2150)) → new_insertBy(:%(Pos(Zero), Neg(Succ(ww3100))), ww41)
new_insertBy072(ww4300, ww44, ww45, ww4600, ww47) → new_insertBy(:%(Neg(Succ(ww45)), Pos(Succ(ww4600))), ww47)
new_insertBy031(Pos(Succ(ww4300)), ww44, ww45, Neg(Succ(ww4600)), ww47, Succ(ww2290)) → new_insertBy065(ww4300, ww44, ww45, ww4600, ww47, new_primPlusNat0(new_primMulNat1(ww4300, ww4600), Succ(ww4600)), ww2290)
new_insertBy034(ww4000000, ww3000, ww3100, ww41, Succ(ww2460)) → new_insertBy(:%(Neg(Succ(ww3000)), Pos(Succ(ww3100))), ww41)
new_insertBy044(Neg(Zero), ww50, ww51, Neg(Succ(ww5200)), ww53, Succ(ww3180)) → new_insertBy(:%(Neg(Succ(ww51)), Neg(Succ(ww5200))), ww53)
new_insertBy055(ww4000000, ww3100, ww41, Succ(ww3970)) → new_insertBy(:%(Neg(Zero), Pos(Succ(ww3100))), ww41)
new_insertBy086(ww2400, ww25, ww26, ww2700, ww28) → new_insertBy(:%(Pos(Succ(ww26)), Neg(Succ(ww2700))), ww28)
new_insertBy050(ww40100, ww3100, ww41, Succ(ww3710)) → new_insertBy(:%(Neg(Zero), Neg(Succ(ww3100))), ww41)
new_insertBy085(ww2400, ww25, ww26, ww2700, ww28, Succ(ww6000), Zero) → new_insertBy086(ww2400, ww25, ww26, ww2700, ww28)
new_insertBy079(ww490, ww50, ww51, ww520, ww53) → new_insertBy(:%(Neg(Succ(ww51)), Neg(ww520)), ww53)
new_insertBy058(ww3000, ww31, ww32, ww3300, ww34, Succ(Succ(ww18500)), Succ(ww14400)) → new_insertBy063(ww3000, ww31, ww32, ww3300, ww34, ww18500, ww14400)
new_insertBy(:%(Neg(Zero), Neg(Succ(ww3100))), :(:%(Pos(Succ(Succ(Zero))), Neg(Succ(ww40100))), ww41)) → new_insertBy050(ww40100, ww3100, ww41, new_primPlusNat0(new_primPlusNat0(Zero, Succ(ww3100)), Succ(ww3100)))
new_insertBy043(ww3100, ww41, Succ(ww3100)) → new_insertBy(:%(Neg(Zero), Pos(Succ(ww3100))), ww41)
new_insertBy013(ww40100, ww3100, ww41, Succ(ww1120)) → new_insertBy(:%(Pos(Zero), Pos(Succ(ww3100))), ww41)
new_insertBy040(ww4000000, ww3100, ww41, Succ(ww3000)) → new_insertBy(:%(Neg(Zero), Neg(Succ(ww3100))), ww41)
new_insertBy068(ww4300, ww44, ww45, ww4600, ww47, Succ(ww2620)) → new_insertBy(:%(Neg(Succ(ww45)), Pos(Succ(ww4600))), ww47)
new_insertBy(:%(Pos(Succ(ww3000)), Pos(Succ(ww3100))), :(:%(Neg(Succ(Succ(Zero))), Pos(Zero)), ww41)) → new_insertBy09(ww3000, ww3100, ww41, new_primPlusNat0(new_primPlusNat0(Zero, Succ(ww3100)), Succ(ww3100)))
new_insertBy011(ww40100, ww3100, ww41, Succ(ww1060)) → new_insertBy(:%(Pos(Zero), Neg(Succ(ww3100))), ww41)
new_insertBy(:%(Pos(Succ(ww3000)), Pos(Succ(ww3100))), :(:%(Neg(Succ(Succ(Succ(ww4000000)))), Pos(Zero)), ww41)) → new_insertBy08(ww4000000, ww3000, ww3100, ww41, new_primPlusNat0(new_primPlusNat0(new_primPlusNat0(new_primMulNat1(ww4000000, ww3100), Succ(ww3100)), Succ(ww3100)), Succ(ww3100)))
new_insertBy032(ww4000000, ww3000, ww3100, ww41, Succ(ww2400)) → new_insertBy(:%(Neg(Succ(ww3000)), Neg(Succ(ww3100))), ww41)
new_insertBy076(ww4900, ww50, ww51, ww5200, ww53, Succ(ww3530)) → new_insertBy080(Succ(ww4900), ww50, ww51, Succ(ww5200), ww53)
new_insertBy01(ww2400, ww25, ww26, ww2700, ww28, Succ(ww6000), Succ(Succ(ww9400))) → new_insertBy085(ww2400, ww25, ww26, ww2700, ww28, ww6000, ww9400)
new_insertBy081(ww4900, ww50, ww51, ww5200, ww53, Succ(ww31800), Zero) → new_insertBy082(ww4900, ww50, ww51, ww5200, ww53)
new_insertBy058(ww3000, ww31, ww32, ww3300, ww34, Succ(Succ(ww18500)), Zero) → new_insertBy064(ww3000, ww31, ww32, ww3300, ww34)
new_insertBy074(ww4900, ww50, ww51, ww5200, ww53, ww3180, Zero) → new_insertBy(:%(Neg(Succ(ww51)), Neg(Succ(ww5200))), ww53)
new_insertBy0(Neg(Zero), ww25, ww26, Neg(Zero), ww28, Succ(ww600)) → new_insertBy(:%(Pos(Succ(ww26)), Neg(Zero)), ww28)
new_insertBy(:%(Pos(Zero), Neg(Succ(ww3100))), :(:%(Pos(Succ(Succ(Succ(ww4000000)))), Neg(Zero)), ww41)) → new_insertBy027(ww4000000, ww3100, ww41, new_primPlusNat0(new_primPlusNat0(new_primPlusNat0(new_primMulNat1(ww4000000, ww3100), Succ(ww3100)), Succ(ww3100)), Succ(ww3100)))
new_insertBy(:%(Pos(Zero), Neg(Succ(ww3100))), :(:%(Pos(Succ(Succ(Succ(ww4000000)))), Neg(Succ(ww40100))), ww41)) → new_insertBy023(ww4000000, ww40100, ww3100, ww41, new_primPlusNat0(new_primPlusNat0(new_primPlusNat0(new_primMulNat1(ww4000000, ww3100), Succ(ww3100)), Succ(ww3100)), Succ(ww3100)))
new_insertBy052(ww40100, ww3100, ww41, Succ(ww3770)) → new_insertBy(:%(Neg(Zero), Pos(Succ(ww3100))), ww41)
new_insertBy(:%(Neg(Succ(ww3000)), ww31), :(:%(ww400, Neg(Succ(ww40100))), ww41)) → new_insertBy044(ww400, ww40100, ww3000, ww31, ww41, new_primPlusNat0(new_primMulNat1(ww3000, ww40100), Succ(ww40100)))
new_insertBy0(Neg(Succ(ww2400)), ww25, ww26, Neg(Zero), ww28, Succ(ww600)) → new_insertBy(:%(Pos(Succ(ww26)), Neg(Zero)), ww28)
new_insertBy070(ww4300, ww44, ww45, ww4600, ww47) → new_insertBy(:%(Neg(Succ(ww45)), Neg(Succ(ww4600))), ww47)
new_insertBy0(Neg(Succ(ww2400)), ww25, ww26, Neg(Succ(ww2700)), ww28, Succ(ww600)) → new_insertBy01(ww2400, ww25, ww26, ww2700, ww28, ww600, new_primPlusNat0(new_primMulNat1(ww2400, ww2700), Succ(ww2700)))
new_insertBy(:%(Neg(Zero), Pos(Succ(ww3100))), :(:%(Neg(Succ(Succ(Succ(ww4000000)))), Neg(Succ(ww40100))), ww41)) → new_insertBy051(ww4000000, ww40100, ww3100, ww41, new_primPlusNat0(new_primPlusNat0(new_primPlusNat0(new_primMulNat1(ww4000000, ww3100), Succ(ww3100)), Succ(ww3100)), Succ(ww3100)))
new_insertBy(:%(Neg(Zero), Pos(Succ(ww3100))), :(:%(Neg(Succ(Succ(Succ(ww4000000)))), Pos(Zero)), ww41)) → new_insertBy042(ww4000000, ww3100, ww41, new_primPlusNat0(new_primPlusNat0(new_primPlusNat0(new_primMulNat1(ww4000000, ww3100), Succ(ww3100)), Succ(ww3100)), Succ(ww3100)))
new_insertBy(:%(Neg(Zero), Neg(Succ(ww3100))), :(:%(Pos(Succ(Zero)), Neg(Zero)), ww41)) → new_insertBy(:%(Neg(Zero), Neg(Succ(ww3100))), ww41)
new_insertBy(:%(Neg(Zero), Pos(Succ(ww3100))), :(:%(Neg(Succ(Zero)), Neg(Succ(ww40100))), ww41)) → new_insertBy(:%(Neg(Zero), Pos(Succ(ww3100))), ww41)
new_insertBy(:%(Pos(Zero), Neg(Succ(ww3100))), :(:%(Pos(Succ(Succ(Zero))), Neg(Succ(ww40100))), ww41)) → new_insertBy024(ww40100, ww3100, ww41, new_primPlusNat0(new_primPlusNat0(Zero, Succ(ww3100)), Succ(ww3100)))
new_insertBy044(Neg(Succ(ww4900)), ww50, ww51, Neg(Succ(ww5200)), ww53, Succ(ww3180)) → new_insertBy074(ww4900, ww50, ww51, ww5200, ww53, ww3180, new_primPlusNat0(new_primMulNat1(ww4900, ww5200), Succ(ww5200)))
new_insertBy065(ww4300, ww44, ww45, ww4600, ww47, Succ(Succ(ww26600)), Zero) → new_insertBy070(ww4300, ww44, ww45, ww4600, ww47)
new_insertBy036(ww4000000, ww40100, ww3100, ww41, Succ(ww2760)) → new_insertBy(:%(Neg(Zero), Neg(Succ(ww3100))), ww41)
new_insertBy044(Pos(ww490), ww50, ww51, Neg(ww520), ww53, Succ(ww3180)) → new_insertBy(:%(Neg(Succ(ww51)), Neg(ww520)), ww53)
new_insertBy04(ww2400, ww25, ww26, ww2700, ww28, Succ(ww6000), Succ(ww9200)) → new_insertBy04(ww2400, ww25, ww26, ww2700, ww28, ww6000, ww9200)
new_insertBy08(ww4000000, ww3000, ww3100, ww41, Succ(ww720)) → new_insertBy(:%(Pos(Succ(ww3000)), Pos(Succ(ww3100))), ww41)
new_insertBy063(ww3000, ww31, ww32, ww3300, ww34, Succ(ww18500), Succ(ww14400)) → new_insertBy063(ww3000, ww31, ww32, ww3300, ww34, ww18500, ww14400)
new_insertBy(:%(Pos(Zero), Neg(Succ(ww3100))), :(:%(Pos(Succ(Zero)), Pos(Succ(ww40100))), ww41)) → new_insertBy(:%(Pos(Zero), Neg(Succ(ww3100))), ww41)
new_insertBy(:%(Pos(Succ(ww3000)), Neg(Succ(ww3100))), :(:%(Pos(Succ(Succ(Succ(ww4000000)))), Pos(Zero)), ww41)) → new_insertBy06(ww4000000, ww3000, ww3100, ww41, new_primPlusNat0(new_primPlusNat0(new_primPlusNat0(new_primMulNat1(ww4000000, ww3100), Succ(ww3100)), Succ(ww3100)), Succ(ww3100)))
new_insertBy017(ww3100, ww41, Succ(ww1360)) → new_insertBy(:%(Pos(Zero), Pos(Succ(ww3100))), ww41)
new_insertBy018(Neg(Succ(ww3000)), ww31, ww32, Pos(Succ(ww3300)), ww34, Succ(ww1440)) → new_insertBy058(ww3000, ww31, ww32, ww3300, ww34, new_primPlusNat0(new_primMulNat1(ww3000, ww3300), Succ(ww3300)), ww1440)
new_insertBy062(ww3000, ww31, ww32, ww3300, ww34) → new_insertBy(:%(Pos(Succ(ww32)), Neg(Succ(ww3300))), ww34)
new_insertBy0(Pos(Succ(ww2400)), ww25, ww26, Neg(Succ(ww2700)), ww28, Zero) → new_insertBy02(ww2400, ww25, ww26, ww2700, ww28, new_primPlusNat0(new_primMulNat1(ww2400, ww2700), Succ(ww2700)))
new_insertBy065(ww4300, ww44, ww45, ww4600, ww47, Succ(Succ(ww26600)), Succ(ww22900)) → new_insertBy069(ww4300, ww44, ww45, ww4600, ww47, ww26600, ww22900)
new_insertBy041(ww3100, ww41, Succ(ww3040)) → new_insertBy(:%(Neg(Zero), Neg(Succ(ww3100))), ww41)
new_insertBy019(ww4000000, ww3000, ww3100, ww41, Succ(ww1570)) → new_insertBy(:%(Pos(Succ(ww3000)), Neg(Succ(ww3100))), ww41)
new_insertBy073(ww4900, ww50, ww51, ww5200, ww53, ww3180, Zero) → new_insertBy(:%(Neg(Succ(ww51)), Pos(Succ(ww5200))), ww53)
new_insertBy03(ww2400, ww25, ww26, ww2700, ww28, Succ(ww880)) → new_insertBy084(Succ(ww2400), ww25, ww26, Succ(ww2700), ww28)
new_insertBy(:%(Neg(Zero), Pos(Succ(ww3100))), :(:%(Neg(Succ(Succ(Succ(ww4000000)))), Pos(Succ(ww40100))), ww41)) → new_insertBy038(ww4000000, ww40100, ww3100, ww41, new_primPlusNat0(new_primPlusNat0(new_primPlusNat0(new_primMulNat1(ww4000000, ww3100), Succ(ww3100)), Succ(ww3100)), Succ(ww3100)))
new_insertBy(:%(Neg(Succ(ww3000)), Neg(Succ(ww3100))), :(:%(Pos(Succ(Succ(Succ(ww4000000)))), Pos(Zero)), ww41)) → new_insertBy032(ww4000000, ww3000, ww3100, ww41, new_primPlusNat0(new_primPlusNat0(new_primPlusNat0(new_primMulNat1(ww4000000, ww3100), Succ(ww3100)), Succ(ww3100)), Succ(ww3100)))
new_insertBy(:%(Neg(Succ(ww3000)), Neg(Succ(ww3100))), :(:%(Pos(Succ(Zero)), Pos(Zero)), ww41)) → new_insertBy(:%(Neg(Succ(ww3000)), Neg(Succ(ww3100))), ww41)
new_insertBy(:%(Neg(Zero), Pos(Succ(ww3100))), :(:%(Neg(Succ(Zero)), Pos(Zero)), ww41)) → new_insertBy(:%(Neg(Zero), Pos(Succ(ww3100))), ww41)
new_insertBy(:%(Pos(Zero), Neg(Succ(ww3100))), :(:%(Pos(Succ(Zero)), Neg(Zero)), ww41)) → new_insertBy(:%(Pos(Zero), Neg(Succ(ww3100))), ww41)
new_insertBy(:%(Pos(Zero), Pos(Succ(ww3100))), :(:%(Neg(Succ(Zero)), Neg(Zero)), ww41)) → new_insertBy(:%(Pos(Zero), Pos(Succ(ww3100))), ww41)
new_insertBy(:%(Neg(Zero), Neg(Succ(ww3100))), :(:%(Pos(Succ(Succ(Succ(ww4000000)))), Neg(Zero)), ww41)) → new_insertBy053(ww4000000, ww3100, ww41, new_primPlusNat0(new_primPlusNat0(new_primPlusNat0(new_primMulNat1(ww4000000, ww3100), Succ(ww3100)), Succ(ww3100)), Succ(ww3100)))
new_insertBy015(ww3100, ww41, Succ(ww1300)) → new_insertBy(:%(Pos(Zero), Neg(Succ(ww3100))), ww41)
new_insertBy044(Neg(Succ(ww4900)), ww50, ww51, Neg(Zero), ww53, Succ(ww3180)) → new_insertBy(:%(Neg(Succ(ww51)), Neg(Zero)), ww53)
new_insertBy033(ww3000, ww3100, ww41, Succ(ww2440)) → new_insertBy(:%(Neg(Succ(ww3000)), Neg(Succ(ww3100))), ww41)
new_insertBy(:%(Pos(Zero), Pos(Succ(ww3100))), :(:%(Neg(Succ(Succ(Zero))), Neg(Zero)), ww41)) → new_insertBy030(ww3100, ww41, new_primPlusNat0(new_primPlusNat0(Zero, Succ(ww3100)), Succ(ww3100)))
new_insertBy(:%(Pos(Zero), Pos(Succ(ww3100))), :(:%(Neg(Succ(Succ(Zero))), Pos(Zero)), ww41)) → new_insertBy017(ww3100, ww41, new_primPlusNat0(new_primPlusNat0(Zero, Succ(ww3100)), Succ(ww3100)))
new_insertBy024(ww40100, ww3100, ww41, Succ(ww1910)) → new_insertBy(:%(Pos(Zero), Neg(Succ(ww3100))), ww41)
new_insertBy030(ww3100, ww41, Succ(ww2210)) → new_insertBy(:%(Pos(Zero), Pos(Succ(ww3100))), ww41)
new_insertBy00(ww2400, ww25, ww26, ww2700, ww28, Succ(ww6000), Succ(Succ(ww9200))) → new_insertBy04(ww2400, ww25, ww26, ww2700, ww28, ww6000, ww9200)
new_insertBy(:%(Neg(Succ(ww3000)), ww31), :(:%(ww400, Pos(Succ(ww40100))), ww41)) → new_insertBy031(ww400, ww40100, ww3000, ww31, ww41, new_primPlusNat0(new_primMulNat1(ww3000, ww40100), Succ(ww40100)))
new_insertBy(:%(Pos(Zero), Pos(Succ(ww3100))), :(:%(Neg(Succ(Succ(Zero))), Neg(Succ(ww40100))), ww41)) → new_insertBy026(ww40100, ww3100, ww41, new_primPlusNat0(new_primPlusNat0(Zero, Succ(ww3100)), Succ(ww3100)))
new_insertBy018(Neg(Succ(ww3000)), ww31, ww32, Pos(Succ(ww3300)), ww34, Zero) → new_insertBy060(ww3000, ww31, ww32, ww3300, ww34, new_primPlusNat0(new_primMulNat1(ww3000, ww3300), Succ(ww3300)))
new_insertBy018(Pos(Succ(ww3000)), ww31, ww32, Neg(Succ(ww3300)), ww34, Zero) → new_insertBy059(ww3000, ww31, ww32, ww3300, ww34, new_primPlusNat0(new_primMulNat1(ww3000, ww3300), Succ(ww3300)))
new_insertBy078(ww4900, ww50, ww51, ww5200, ww53) → new_insertBy(:%(Neg(Succ(ww51)), Pos(Succ(ww5200))), ww53)
new_insertBy0(Neg(ww240), ww25, ww26, Pos(ww270), ww28, Succ(ww600)) → new_insertBy(:%(Pos(Succ(ww26)), Pos(ww270)), ww28)
new_insertBy00(ww2400, ww25, ww26, ww2700, ww28, ww600, Zero) → new_insertBy(:%(Pos(Succ(ww26)), Pos(Succ(ww2700))), ww28)
new_insertBy075(ww4900, ww50, ww51, ww5200, ww53, Succ(ww3510)) → new_insertBy079(Succ(ww4900), ww50, ww51, Succ(ww5200), ww53)
new_insertBy01(ww2400, ww25, ww26, ww2700, ww28, Succ(ww6000), Succ(Zero)) → new_insertBy086(ww2400, ww25, ww26, ww2700, ww28)
new_insertBy044(Pos(Succ(ww4900)), ww50, ww51, Pos(Zero), ww53, Succ(ww3180)) → new_insertBy(:%(Neg(Succ(ww51)), Pos(Zero)), ww53)
new_insertBy(:%(Neg(Zero), Pos(Succ(ww3100))), :(:%(Neg(Succ(Zero)), Pos(Succ(ww40100))), ww41)) → new_insertBy(:%(Neg(Zero), Pos(Succ(ww3100))), ww41)
new_insertBy(:%(Pos(Zero), Neg(Succ(ww3100))), :(:%(Pos(Succ(Zero)), Neg(Succ(ww40100))), ww41)) → new_insertBy(:%(Pos(Zero), Neg(Succ(ww3100))), ww41)
new_insertBy(:%(Neg(Succ(ww3000)), Pos(Succ(ww3100))), :(:%(Neg(Succ(Zero)), Pos(Zero)), ww41)) → new_insertBy(:%(Neg(Succ(ww3000)), Pos(Succ(ww3100))), ww41)
new_insertBy(:%(Pos(Zero), Pos(Succ(ww3100))), :(:%(Neg(Succ(Succ(Succ(ww4000000)))), Pos(Zero)), ww41)) → new_insertBy016(ww4000000, ww3100, ww41, new_primPlusNat0(new_primPlusNat0(new_primPlusNat0(new_primMulNat1(ww4000000, ww3100), Succ(ww3100)), Succ(ww3100)), Succ(ww3100)))
new_insertBy(:%(Pos(Succ(ww3000)), Neg(Succ(ww3100))), :(:%(Pos(Succ(Succ(Zero))), Neg(Zero)), ww41)) → new_insertBy020(ww3000, ww3100, ww41, new_primPlusNat0(new_primPlusNat0(Zero, Succ(ww3100)), Succ(ww3100)))
new_insertBy(:%(Pos(Succ(ww3000)), Neg(Succ(ww3100))), :(:%(Pos(Succ(Zero)), Neg(Zero)), ww41)) → new_insertBy(:%(Pos(Succ(ww3000)), Neg(Succ(ww3100))), ww41)
new_insertBy066(ww4300, ww44, ww45, ww4600, ww47, Succ(Succ(ww26800)), Zero) → new_insertBy072(ww4300, ww44, ww45, ww4600, ww47)
new_insertBy(:%(Pos(Zero), Pos(Succ(ww3100))), :(:%(Neg(Succ(Succ(Zero))), Pos(Succ(ww40100))), ww41)) → new_insertBy013(ww40100, ww3100, ww41, new_primPlusNat0(new_primPlusNat0(Zero, Succ(ww3100)), Succ(ww3100)))
new_insertBy031(Neg(Succ(ww4300)), ww44, ww45, Pos(Succ(ww4600)), ww47, Succ(ww2290)) → new_insertBy066(ww4300, ww44, ww45, ww4600, ww47, new_primPlusNat0(new_primMulNat1(ww4300, ww4600), Succ(ww4600)), ww2290)
new_insertBy053(ww4000000, ww3100, ww41, Succ(ww3910)) → new_insertBy(:%(Neg(Zero), Neg(Succ(ww3100))), ww41)
new_insertBy0(Pos(ww240), ww25, ww26, Neg(ww270), ww28, Succ(ww600)) → new_insertBy(:%(Pos(Succ(ww26)), Neg(ww270)), ww28)
new_insertBy063(ww3000, ww31, ww32, ww3300, ww34, Succ(ww18500), Zero) → new_insertBy064(ww3000, ww31, ww32, ww3300, ww34)
new_insertBy061(ww3000, ww31, ww32, ww3300, ww34, Succ(ww18300), Zero) → new_insertBy062(ww3000, ww31, ww32, ww3300, ww34)
new_insertBy022(ww3000, ww3100, ww41, Succ(ww1670)) → new_insertBy(:%(Pos(Succ(ww3000)), Pos(Succ(ww3100))), ww41)
new_insertBy039(ww40100, ww3100, ww41, Succ(ww2860)) → new_insertBy(:%(Neg(Zero), Pos(Succ(ww3100))), ww41)
new_insertBy09(ww3000, ww3100, ww41, Succ(ww760)) → new_insertBy(:%(Pos(Succ(ww3000)), Pos(Succ(ww3100))), ww41)
new_insertBy080(ww490, ww50, ww51, ww520, ww53) → new_insertBy(:%(Neg(Succ(ww51)), Pos(ww520)), ww53)
new_insertBy077(ww4900, ww50, ww51, ww5200, ww53, Succ(ww31800), Zero) → new_insertBy078(ww4900, ww50, ww51, ww5200, ww53)
new_insertBy0(Pos(Succ(ww2400)), ww25, ww26, Pos(Zero), ww28, Succ(ww600)) → new_insertBy(:%(Pos(Succ(ww26)), Pos(Zero)), ww28)
new_insertBy031(Neg(Succ(ww4300)), ww44, ww45, Pos(Succ(ww4600)), ww47, Zero) → new_insertBy068(ww4300, ww44, ww45, ww4600, ww47, new_primPlusNat0(new_primMulNat1(ww4300, ww4600), Succ(ww4600)))
new_insertBy(:%(Pos(Succ(ww3000)), Neg(Succ(ww3100))), :(:%(Pos(Succ(Succ(Succ(ww4000000)))), Neg(Zero)), ww41)) → new_insertBy019(ww4000000, ww3000, ww3100, ww41, new_primPlusNat0(new_primPlusNat0(new_primPlusNat0(new_primMulNat1(ww4000000, ww3100), Succ(ww3100)), Succ(ww3100)), Succ(ww3100)))
new_insertBy042(ww4000000, ww3100, ww41, Succ(ww3060)) → new_insertBy(:%(Neg(Zero), Pos(Succ(ww3100))), ww41)
new_insertBy044(Neg(Zero), ww50, ww51, Neg(Zero), ww53, Succ(ww3180)) → new_insertBy(:%(Neg(Succ(ww51)), Neg(Zero)), ww53)
new_insertBy073(ww4900, ww50, ww51, ww5200, ww53, Succ(ww31800), Succ(Succ(ww35700))) → new_insertBy077(ww4900, ww50, ww51, ww5200, ww53, ww31800, ww35700)
new_insertBy(:%(Pos(Succ(ww3000)), Pos(Succ(ww3100))), :(:%(Neg(Succ(Zero)), Pos(Zero)), ww41)) → new_insertBy(:%(Pos(Succ(ww3000)), Pos(Succ(ww3100))), ww41)
new_insertBy060(ww3000, ww31, ww32, ww3300, ww34, Succ(ww1790)) → new_insertBy(:%(Pos(Succ(ww32)), Pos(Succ(ww3300))), ww34)
new_insertBy(:%(Neg(Zero), Neg(Succ(ww3100))), :(:%(Pos(Succ(Zero)), Neg(Succ(ww40100))), ww41)) → new_insertBy(:%(Neg(Zero), Neg(Succ(ww3100))), ww41)
new_insertBy(:%(Pos(Zero), Pos(Succ(ww3100))), :(:%(Neg(Succ(Succ(Succ(ww4000000)))), Neg(Zero)), ww41)) → new_insertBy029(ww4000000, ww3100, ww41, new_primPlusNat0(new_primPlusNat0(new_primPlusNat0(new_primMulNat1(ww4000000, ww3100), Succ(ww3100)), Succ(ww3100)), Succ(ww3100)))
new_insertBy(:%(Pos(Zero), Neg(Succ(ww3100))), :(:%(Pos(Succ(Succ(Zero))), Pos(Zero)), ww41)) → new_insertBy015(ww3100, ww41, new_primPlusNat0(new_primPlusNat0(Zero, Succ(ww3100)), Succ(ww3100)))
new_insertBy071(ww4300, ww44, ww45, ww4600, ww47, Succ(ww26800), Zero) → new_insertBy072(ww4300, ww44, ww45, ww4600, ww47)
new_insertBy04(ww2400, ww25, ww26, ww2700, ww28, Succ(ww6000), Zero) → new_insertBy05(ww2400, ww25, ww26, ww2700, ww28)
new_insertBy029(ww4000000, ww3100, ww41, Succ(ww2170)) → new_insertBy(:%(Pos(Zero), Pos(Succ(ww3100))), ww41)
new_insertBy(:%(Pos(Succ(ww3000)), Pos(Succ(ww3100))), :(:%(Neg(Succ(Zero)), Neg(Zero)), ww41)) → new_insertBy(:%(Pos(Succ(ww3000)), Pos(Succ(ww3100))), ww41)
new_insertBy(:%(Pos(Succ(ww3000)), ww31), :(:%(ww400, Neg(Succ(ww40100))), ww41)) → new_insertBy018(ww400, ww40100, ww3000, ww31, ww41, new_primPlusNat0(new_primMulNat1(ww3000, ww40100), Succ(ww40100)))
new_insertBy(:%(Neg(Zero), Pos(Succ(ww3100))), :(:%(Neg(Succ(Zero)), Neg(Zero)), ww41)) → new_insertBy(:%(Neg(Zero), Pos(Succ(ww3100))), ww41)
new_insertBy(:%(Pos(Zero), Neg(Succ(ww3100))), :(:%(Pos(Succ(Succ(Zero))), Pos(Succ(ww40100))), ww41)) → new_insertBy011(ww40100, ww3100, ww41, new_primPlusNat0(new_primPlusNat0(Zero, Succ(ww3100)), Succ(ww3100)))
new_insertBy(:%(Neg(Zero), Pos(Succ(ww3100))), :(:%(Neg(Succ(Succ(Zero))), Pos(Succ(ww40100))), ww41)) → new_insertBy039(ww40100, ww3100, ww41, new_primPlusNat0(new_primPlusNat0(Zero, Succ(ww3100)), Succ(ww3100)))
new_insertBy057(ww3000, ww31, ww32, ww3300, ww34, Succ(Succ(ww18300)), Zero) → new_insertBy062(ww3000, ww31, ww32, ww3300, ww34)
new_insertBy085(ww2400, ww25, ww26, ww2700, ww28, Succ(ww6000), Succ(ww9400)) → new_insertBy085(ww2400, ww25, ww26, ww2700, ww28, ww6000, ww9400)
new_insertBy044(Neg(ww490), ww50, ww51, Pos(ww520), ww53, Succ(ww3180)) → new_insertBy(:%(Neg(Succ(ww51)), Pos(ww520)), ww53)
new_insertBy(:%(Neg(Zero), Pos(Succ(ww3100))), :(:%(Neg(Succ(Succ(Zero))), Neg(Succ(ww40100))), ww41)) → new_insertBy052(ww40100, ww3100, ww41, new_primPlusNat0(new_primPlusNat0(Zero, Succ(ww3100)), Succ(ww3100)))
new_insertBy05(ww2400, ww25, ww26, ww2700, ww28) → new_insertBy(:%(Pos(Succ(ww26)), Pos(Succ(ww2700))), ww28)
new_insertBy(:%(Pos(Succ(ww3000)), Neg(Succ(ww3100))), :(:%(Pos(Succ(Succ(Zero))), Pos(Zero)), ww41)) → new_insertBy07(ww3000, ww3100, ww41, new_primPlusNat0(new_primPlusNat0(Zero, Succ(ww3100)), Succ(ww3100)))
new_insertBy(:%(Neg(Zero), Neg(Succ(ww3100))), :(:%(Pos(Succ(Succ(Zero))), Pos(Zero)), ww41)) → new_insertBy041(ww3100, ww41, new_primPlusNat0(new_primPlusNat0(Zero, Succ(ww3100)), Succ(ww3100)))
new_insertBy(:%(Pos(Zero), Neg(Succ(ww3100))), :(:%(Pos(Succ(Succ(Succ(ww4000000)))), Pos(Succ(ww40100))), ww41)) → new_insertBy010(ww4000000, ww40100, ww3100, ww41, new_primPlusNat0(new_primPlusNat0(new_primPlusNat0(new_primMulNat1(ww4000000, ww3100), Succ(ww3100)), Succ(ww3100)), Succ(ww3100)))
new_insertBy(:%(Pos(Succ(ww3000)), ww31), :(:%(ww400, Pos(Succ(ww40100))), ww41)) → new_insertBy0(ww400, ww40100, ww3000, ww31, ww41, new_primPlusNat1(new_primMulNat1(ww3000, ww40100), ww40100))
new_insertBy(:%(Pos(Zero), Pos(Succ(ww3100))), :(:%(Neg(Succ(Zero)), Pos(Succ(ww40100))), ww41)) → new_insertBy(:%(Pos(Zero), Pos(Succ(ww3100))), ww41)
new_insertBy047(ww4000000, ww3000, ww3100, ww41, Succ(ww3370)) → new_insertBy(:%(Neg(Succ(ww3000)), Pos(Succ(ww3100))), ww41)
new_insertBy027(ww4000000, ww3100, ww41, Succ(ww2110)) → new_insertBy(:%(Pos(Zero), Neg(Succ(ww3100))), ww41)
new_insertBy071(ww4300, ww44, ww45, ww4600, ww47, Succ(ww26800), Succ(ww22900)) → new_insertBy071(ww4300, ww44, ww45, ww4600, ww47, ww26800, ww22900)
new_insertBy018(Pos(Succ(ww3000)), ww31, ww32, Neg(Succ(ww3300)), ww34, Succ(ww1440)) → new_insertBy057(ww3000, ww31, ww32, ww3300, ww34, new_primPlusNat0(new_primMulNat1(ww3000, ww3300), Succ(ww3300)), ww1440)
new_insertBy(:%(Neg(Zero), Pos(Succ(ww3100))), :(:%(Neg(Succ(Succ(Zero))), Neg(Zero)), ww41)) → new_insertBy056(ww3100, ww41, new_primPlusNat0(new_primPlusNat0(Zero, Succ(ww3100)), Succ(ww3100)))
new_insertBy(:%(Neg(Zero), Neg(Succ(ww3100))), :(:%(Pos(Succ(Succ(Zero))), Neg(Zero)), ww41)) → new_insertBy054(ww3100, ww41, new_primPlusNat0(new_primPlusNat0(Zero, Succ(ww3100)), Succ(ww3100)))
new_insertBy056(ww3100, ww41, Succ(ww4010)) → new_insertBy(:%(Neg(Zero), Pos(Succ(ww3100))), ww41)
new_insertBy0(Neg(Zero), ww25, ww26, Neg(Succ(ww2700)), ww28, Succ(ww600)) → new_insertBy(:%(Pos(Succ(ww26)), Neg(Succ(ww2700))), ww28)
new_insertBy064(ww3000, ww31, ww32, ww3300, ww34) → new_insertBy(:%(Pos(Succ(ww32)), Pos(Succ(ww3300))), ww34)
new_insertBy023(ww4000000, ww40100, ww3100, ww41, Succ(ww1870)) → new_insertBy(:%(Pos(Zero), Neg(Succ(ww3100))), ww41)
new_insertBy044(Pos(Succ(ww4900)), ww50, ww51, Pos(Succ(ww5200)), ww53, Succ(ww3180)) → new_insertBy073(ww4900, ww50, ww51, ww5200, ww53, ww3180, new_primPlusNat0(new_primMulNat1(ww4900, ww5200), Succ(ww5200)))
new_insertBy(:%(Pos(Zero), Neg(Succ(ww3100))), :(:%(Pos(Succ(Zero)), Pos(Zero)), ww41)) → new_insertBy(:%(Pos(Zero), Neg(Succ(ww3100))), ww41)
new_insertBy066(ww4300, ww44, ww45, ww4600, ww47, Succ(Succ(ww26800)), Succ(ww22900)) → new_insertBy071(ww4300, ww44, ww45, ww4600, ww47, ww26800, ww22900)
new_insertBy025(ww4000000, ww40100, ww3100, ww41, Succ(ww1930)) → new_insertBy(:%(Pos(Zero), Pos(Succ(ww3100))), ww41)
new_insertBy0(Pos(Zero), ww25, ww26, Pos(Succ(ww2700)), ww28, Succ(ww600)) → new_insertBy(:%(Pos(Succ(ww26)), Pos(Succ(ww2700))), ww28)
new_insertBy06(ww4000000, ww3000, ww3100, ww41, Succ(ww660)) → new_insertBy(:%(Pos(Succ(ww3000)), Neg(Succ(ww3100))), ww41)
new_insertBy026(ww40100, ww3100, ww41, Succ(ww1970)) → new_insertBy(:%(Pos(Zero), Pos(Succ(ww3100))), ww41)
new_insertBy01(ww2400, ww25, ww26, ww2700, ww28, ww600, Zero) → new_insertBy(:%(Pos(Succ(ww26)), Neg(Succ(ww2700))), ww28)
new_insertBy(:%(Pos(Zero), Pos(Succ(ww3100))), :(:%(Neg(Succ(Zero)), Neg(Succ(ww40100))), ww41)) → new_insertBy(:%(Pos(Zero), Pos(Succ(ww3100))), ww41)
new_insertBy(:%(Neg(Succ(ww3000)), Pos(Succ(ww3100))), :(:%(Neg(Succ(Succ(Succ(ww4000000)))), Pos(Zero)), ww41)) → new_insertBy034(ww4000000, ww3000, ww3100, ww41, new_primPlusNat0(new_primPlusNat0(new_primPlusNat0(new_primMulNat1(ww4000000, ww3100), Succ(ww3100)), Succ(ww3100)), Succ(ww3100)))
new_insertBy020(ww3000, ww3100, ww41, Succ(ww1610)) → new_insertBy(:%(Pos(Succ(ww3000)), Neg(Succ(ww3100))), ww41)
new_insertBy(:%(Neg(Zero), Pos(Succ(ww3100))), :(:%(Neg(Succ(Succ(Succ(ww4000000)))), Neg(Zero)), ww41)) → new_insertBy055(ww4000000, ww3100, ww41, new_primPlusNat0(new_primPlusNat0(new_primPlusNat0(new_primMulNat1(ww4000000, ww3100), Succ(ww3100)), Succ(ww3100)), Succ(ww3100)))
new_insertBy082(ww4900, ww50, ww51, ww5200, ww53) → new_insertBy(:%(Neg(Succ(ww51)), Neg(Succ(ww5200))), ww53)
new_insertBy0(Pos(Zero), ww25, ww26, Pos(Zero), ww28, Succ(ww600)) → new_insertBy(:%(Pos(Succ(ww26)), Pos(Zero)), ww28)
new_insertBy054(ww3100, ww41, Succ(ww3950)) → new_insertBy(:%(Neg(Zero), Neg(Succ(ww3100))), ww41)
The TRS R consists of the following rules:
new_primPlusNat1(Zero, ww40100) → Succ(ww40100)
new_primPlusNat0(Zero, Zero) → Zero
new_primMulNat1(Zero, ww40100) → Zero
new_primPlusNat1(Succ(ww590), ww40100) → Succ(Succ(new_primPlusNat0(ww590, ww40100)))
new_primPlusNat0(Succ(ww5900), Zero) → Succ(ww5900)
new_primPlusNat0(Zero, Succ(ww401000)) → Succ(ww401000)
new_primPlusNat0(Succ(ww5900), Succ(ww401000)) → Succ(Succ(new_primPlusNat0(ww5900, ww401000)))
new_primMulNat1(Succ(ww30000), ww40100) → new_primPlusNat1(new_primMulNat1(ww30000, ww40100), ww40100)
The set Q consists of the following terms:
new_primMulNat1(Succ(x0), x1)
new_primPlusNat0(Zero, Zero)
new_primPlusNat0(Succ(x0), Zero)
new_primPlusNat0(Zero, Succ(x0))
new_primPlusNat1(Zero, x0)
new_primPlusNat0(Succ(x0), Succ(x1))
new_primMulNat1(Zero, x0)
new_primPlusNat1(Succ(x0), x1)
We have to consider all minimal (P,Q,R)-chains.
The approximation of the Dependency Graph [15,17,22] contains 6 SCCs.
↳ HASKELL
↳ CR
↳ HASKELL
↳ BR
↳ HASKELL
↳ COR
↳ HASKELL
↳ Narrow
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDPSizeChangeProof
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
Q DP problem:
The TRS P consists of the following rules:
new_insertBy(:%(Pos(Zero), Pos(Succ(ww3100))), :(:%(Neg(Succ(Succ(Succ(ww4000000)))), Neg(Succ(ww40100))), ww41)) → new_insertBy025(ww4000000, ww40100, ww3100, ww41, new_primPlusNat0(new_primPlusNat0(new_primPlusNat0(new_primMulNat1(ww4000000, ww3100), Succ(ww3100)), Succ(ww3100)), Succ(ww3100)))
new_insertBy030(ww3100, ww41, Succ(ww2210)) → new_insertBy(:%(Pos(Zero), Pos(Succ(ww3100))), ww41)
new_insertBy(:%(Pos(Zero), Pos(Succ(ww3100))), :(:%(Neg(Succ(Zero)), Pos(Succ(ww40100))), ww41)) → new_insertBy(:%(Pos(Zero), Pos(Succ(ww3100))), ww41)
new_insertBy(:%(Pos(Zero), Pos(Succ(ww3100))), :(:%(Neg(Succ(Zero)), Pos(Zero)), ww41)) → new_insertBy(:%(Pos(Zero), Pos(Succ(ww3100))), ww41)
new_insertBy017(ww3100, ww41, Succ(ww1360)) → new_insertBy(:%(Pos(Zero), Pos(Succ(ww3100))), ww41)
new_insertBy025(ww4000000, ww40100, ww3100, ww41, Succ(ww1930)) → new_insertBy(:%(Pos(Zero), Pos(Succ(ww3100))), ww41)
new_insertBy(:%(Pos(Zero), Pos(Succ(ww3100))), :(:%(Neg(Succ(Succ(Zero))), Neg(Succ(ww40100))), ww41)) → new_insertBy026(ww40100, ww3100, ww41, new_primPlusNat0(new_primPlusNat0(Zero, Succ(ww3100)), Succ(ww3100)))
new_insertBy(:%(Pos(Zero), Pos(Succ(ww3100))), :(:%(Neg(Succ(Succ(Succ(ww4000000)))), Pos(Zero)), ww41)) → new_insertBy016(ww4000000, ww3100, ww41, new_primPlusNat0(new_primPlusNat0(new_primPlusNat0(new_primMulNat1(ww4000000, ww3100), Succ(ww3100)), Succ(ww3100)), Succ(ww3100)))
new_insertBy026(ww40100, ww3100, ww41, Succ(ww1970)) → new_insertBy(:%(Pos(Zero), Pos(Succ(ww3100))), ww41)
new_insertBy(:%(Pos(Zero), Pos(Succ(ww3100))), :(:%(Neg(Succ(Zero)), Neg(Succ(ww40100))), ww41)) → new_insertBy(:%(Pos(Zero), Pos(Succ(ww3100))), ww41)
new_insertBy(:%(Pos(Zero), Pos(Succ(ww3100))), :(:%(Neg(Succ(Succ(Succ(ww4000000)))), Neg(Zero)), ww41)) → new_insertBy029(ww4000000, ww3100, ww41, new_primPlusNat0(new_primPlusNat0(new_primPlusNat0(new_primMulNat1(ww4000000, ww3100), Succ(ww3100)), Succ(ww3100)), Succ(ww3100)))
new_insertBy(:%(Pos(Zero), Pos(Succ(ww3100))), :(:%(Neg(Succ(Succ(Zero))), Pos(Succ(ww40100))), ww41)) → new_insertBy013(ww40100, ww3100, ww41, new_primPlusNat0(new_primPlusNat0(Zero, Succ(ww3100)), Succ(ww3100)))
new_insertBy(:%(Pos(Zero), Pos(Succ(ww3100))), :(:%(Neg(Succ(Zero)), Neg(Zero)), ww41)) → new_insertBy(:%(Pos(Zero), Pos(Succ(ww3100))), ww41)
new_insertBy016(ww4000000, ww3100, ww41, Succ(ww1320)) → new_insertBy(:%(Pos(Zero), Pos(Succ(ww3100))), ww41)
new_insertBy029(ww4000000, ww3100, ww41, Succ(ww2170)) → new_insertBy(:%(Pos(Zero), Pos(Succ(ww3100))), ww41)
new_insertBy(:%(Pos(Zero), Pos(Succ(ww3100))), :(:%(Neg(Succ(Succ(Succ(ww4000000)))), Pos(Succ(ww40100))), ww41)) → new_insertBy012(ww4000000, ww40100, ww3100, ww41, new_primPlusNat0(new_primPlusNat0(new_primPlusNat0(new_primMulNat1(ww4000000, ww3100), Succ(ww3100)), Succ(ww3100)), Succ(ww3100)))
new_insertBy(:%(Pos(Zero), Pos(Succ(ww3100))), :(:%(Neg(Succ(Succ(Zero))), Neg(Zero)), ww41)) → new_insertBy030(ww3100, ww41, new_primPlusNat0(new_primPlusNat0(Zero, Succ(ww3100)), Succ(ww3100)))
new_insertBy(:%(Pos(Zero), Pos(Succ(ww3100))), :(:%(Neg(Succ(Succ(Zero))), Pos(Zero)), ww41)) → new_insertBy017(ww3100, ww41, new_primPlusNat0(new_primPlusNat0(Zero, Succ(ww3100)), Succ(ww3100)))
new_insertBy013(ww40100, ww3100, ww41, Succ(ww1120)) → new_insertBy(:%(Pos(Zero), Pos(Succ(ww3100))), ww41)
new_insertBy012(ww4000000, ww40100, ww3100, ww41, Succ(ww1080)) → new_insertBy(:%(Pos(Zero), Pos(Succ(ww3100))), ww41)
The TRS R consists of the following rules:
new_primPlusNat1(Zero, ww40100) → Succ(ww40100)
new_primPlusNat0(Zero, Zero) → Zero
new_primMulNat1(Zero, ww40100) → Zero
new_primPlusNat1(Succ(ww590), ww40100) → Succ(Succ(new_primPlusNat0(ww590, ww40100)))
new_primPlusNat0(Succ(ww5900), Zero) → Succ(ww5900)
new_primPlusNat0(Zero, Succ(ww401000)) → Succ(ww401000)
new_primPlusNat0(Succ(ww5900), Succ(ww401000)) → Succ(Succ(new_primPlusNat0(ww5900, ww401000)))
new_primMulNat1(Succ(ww30000), ww40100) → new_primPlusNat1(new_primMulNat1(ww30000, ww40100), ww40100)
The set Q consists of the following terms:
new_primMulNat1(Succ(x0), x1)
new_primPlusNat0(Zero, Zero)
new_primPlusNat0(Succ(x0), Zero)
new_primPlusNat0(Zero, Succ(x0))
new_primPlusNat1(Zero, x0)
new_primPlusNat0(Succ(x0), Succ(x1))
new_primMulNat1(Zero, x0)
new_primPlusNat1(Succ(x0), x1)
We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem. From the DPs we obtained the following set of size-change graphs:
- new_insertBy025(ww4000000, ww40100, ww3100, ww41, Succ(ww1930)) → new_insertBy(:%(Pos(Zero), Pos(Succ(ww3100))), ww41)
The graph contains the following edges 4 >= 2
- new_insertBy(:%(Pos(Zero), Pos(Succ(ww3100))), :(:%(Neg(Succ(Succ(Succ(ww4000000)))), Neg(Succ(ww40100))), ww41)) → new_insertBy025(ww4000000, ww40100, ww3100, ww41, new_primPlusNat0(new_primPlusNat0(new_primPlusNat0(new_primMulNat1(ww4000000, ww3100), Succ(ww3100)), Succ(ww3100)), Succ(ww3100)))
The graph contains the following edges 2 > 1, 2 > 2, 1 > 3, 2 > 4
- new_insertBy012(ww4000000, ww40100, ww3100, ww41, Succ(ww1080)) → new_insertBy(:%(Pos(Zero), Pos(Succ(ww3100))), ww41)
The graph contains the following edges 4 >= 2
- new_insertBy(:%(Pos(Zero), Pos(Succ(ww3100))), :(:%(Neg(Succ(Succ(Succ(ww4000000)))), Pos(Succ(ww40100))), ww41)) → new_insertBy012(ww4000000, ww40100, ww3100, ww41, new_primPlusNat0(new_primPlusNat0(new_primPlusNat0(new_primMulNat1(ww4000000, ww3100), Succ(ww3100)), Succ(ww3100)), Succ(ww3100)))
The graph contains the following edges 2 > 1, 2 > 2, 1 > 3, 2 > 4
- new_insertBy030(ww3100, ww41, Succ(ww2210)) → new_insertBy(:%(Pos(Zero), Pos(Succ(ww3100))), ww41)
The graph contains the following edges 2 >= 2
- new_insertBy(:%(Pos(Zero), Pos(Succ(ww3100))), :(:%(Neg(Succ(Succ(Zero))), Neg(Zero)), ww41)) → new_insertBy030(ww3100, ww41, new_primPlusNat0(new_primPlusNat0(Zero, Succ(ww3100)), Succ(ww3100)))
The graph contains the following edges 1 > 1, 2 > 2
- new_insertBy017(ww3100, ww41, Succ(ww1360)) → new_insertBy(:%(Pos(Zero), Pos(Succ(ww3100))), ww41)
The graph contains the following edges 2 >= 2
- new_insertBy(:%(Pos(Zero), Pos(Succ(ww3100))), :(:%(Neg(Succ(Succ(Zero))), Pos(Zero)), ww41)) → new_insertBy017(ww3100, ww41, new_primPlusNat0(new_primPlusNat0(Zero, Succ(ww3100)), Succ(ww3100)))
The graph contains the following edges 1 > 1, 2 > 2
- new_insertBy026(ww40100, ww3100, ww41, Succ(ww1970)) → new_insertBy(:%(Pos(Zero), Pos(Succ(ww3100))), ww41)
The graph contains the following edges 3 >= 2
- new_insertBy(:%(Pos(Zero), Pos(Succ(ww3100))), :(:%(Neg(Succ(Succ(Zero))), Neg(Succ(ww40100))), ww41)) → new_insertBy026(ww40100, ww3100, ww41, new_primPlusNat0(new_primPlusNat0(Zero, Succ(ww3100)), Succ(ww3100)))
The graph contains the following edges 2 > 1, 1 > 2, 2 > 3
- new_insertBy016(ww4000000, ww3100, ww41, Succ(ww1320)) → new_insertBy(:%(Pos(Zero), Pos(Succ(ww3100))), ww41)
The graph contains the following edges 3 >= 2
- new_insertBy(:%(Pos(Zero), Pos(Succ(ww3100))), :(:%(Neg(Succ(Succ(Succ(ww4000000)))), Pos(Zero)), ww41)) → new_insertBy016(ww4000000, ww3100, ww41, new_primPlusNat0(new_primPlusNat0(new_primPlusNat0(new_primMulNat1(ww4000000, ww3100), Succ(ww3100)), Succ(ww3100)), Succ(ww3100)))
The graph contains the following edges 2 > 1, 1 > 2, 2 > 3
- new_insertBy013(ww40100, ww3100, ww41, Succ(ww1120)) → new_insertBy(:%(Pos(Zero), Pos(Succ(ww3100))), ww41)
The graph contains the following edges 3 >= 2
- new_insertBy029(ww4000000, ww3100, ww41, Succ(ww2170)) → new_insertBy(:%(Pos(Zero), Pos(Succ(ww3100))), ww41)
The graph contains the following edges 3 >= 2
- new_insertBy(:%(Pos(Zero), Pos(Succ(ww3100))), :(:%(Neg(Succ(Succ(Zero))), Pos(Succ(ww40100))), ww41)) → new_insertBy013(ww40100, ww3100, ww41, new_primPlusNat0(new_primPlusNat0(Zero, Succ(ww3100)), Succ(ww3100)))
The graph contains the following edges 2 > 1, 1 > 2, 2 > 3
- new_insertBy(:%(Pos(Zero), Pos(Succ(ww3100))), :(:%(Neg(Succ(Succ(Succ(ww4000000)))), Neg(Zero)), ww41)) → new_insertBy029(ww4000000, ww3100, ww41, new_primPlusNat0(new_primPlusNat0(new_primPlusNat0(new_primMulNat1(ww4000000, ww3100), Succ(ww3100)), Succ(ww3100)), Succ(ww3100)))
The graph contains the following edges 2 > 1, 1 > 2, 2 > 3
- new_insertBy(:%(Pos(Zero), Pos(Succ(ww3100))), :(:%(Neg(Succ(Zero)), Pos(Zero)), ww41)) → new_insertBy(:%(Pos(Zero), Pos(Succ(ww3100))), ww41)
The graph contains the following edges 1 >= 1, 2 > 2
- new_insertBy(:%(Pos(Zero), Pos(Succ(ww3100))), :(:%(Neg(Succ(Zero)), Neg(Zero)), ww41)) → new_insertBy(:%(Pos(Zero), Pos(Succ(ww3100))), ww41)
The graph contains the following edges 1 >= 1, 2 > 2
- new_insertBy(:%(Pos(Zero), Pos(Succ(ww3100))), :(:%(Neg(Succ(Zero)), Pos(Succ(ww40100))), ww41)) → new_insertBy(:%(Pos(Zero), Pos(Succ(ww3100))), ww41)
The graph contains the following edges 1 >= 1, 2 > 2
- new_insertBy(:%(Pos(Zero), Pos(Succ(ww3100))), :(:%(Neg(Succ(Zero)), Neg(Succ(ww40100))), ww41)) → new_insertBy(:%(Pos(Zero), Pos(Succ(ww3100))), ww41)
The graph contains the following edges 1 >= 1, 2 > 2
↳ HASKELL
↳ CR
↳ HASKELL
↳ BR
↳ HASKELL
↳ COR
↳ HASKELL
↳ Narrow
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDPSizeChangeProof
↳ QDP
↳ QDP
↳ QDP
↳ QDP
Q DP problem:
The TRS P consists of the following rules:
new_insertBy(:%(Neg(Zero), Pos(Succ(ww3100))), :(:%(Neg(Succ(Succ(Succ(ww4000000)))), Pos(Succ(ww40100))), ww41)) → new_insertBy038(ww4000000, ww40100, ww3100, ww41, new_primPlusNat0(new_primPlusNat0(new_primPlusNat0(new_primMulNat1(ww4000000, ww3100), Succ(ww3100)), Succ(ww3100)), Succ(ww3100)))
new_insertBy(:%(Neg(Zero), Pos(Succ(ww3100))), :(:%(Neg(Succ(Succ(Zero))), Pos(Succ(ww40100))), ww41)) → new_insertBy039(ww40100, ww3100, ww41, new_primPlusNat0(new_primPlusNat0(Zero, Succ(ww3100)), Succ(ww3100)))
new_insertBy038(ww4000000, ww40100, ww3100, ww41, Succ(ww2820)) → new_insertBy(:%(Neg(Zero), Pos(Succ(ww3100))), ww41)
new_insertBy(:%(Neg(Zero), Pos(Succ(ww3100))), :(:%(Neg(Succ(Succ(Zero))), Neg(Succ(ww40100))), ww41)) → new_insertBy052(ww40100, ww3100, ww41, new_primPlusNat0(new_primPlusNat0(Zero, Succ(ww3100)), Succ(ww3100)))
new_insertBy051(ww4000000, ww40100, ww3100, ww41, Succ(ww3730)) → new_insertBy(:%(Neg(Zero), Pos(Succ(ww3100))), ww41)
new_insertBy(:%(Neg(Zero), Pos(Succ(ww3100))), :(:%(Neg(Succ(Zero)), Pos(Zero)), ww41)) → new_insertBy(:%(Neg(Zero), Pos(Succ(ww3100))), ww41)
new_insertBy(:%(Neg(Zero), Pos(Succ(ww3100))), :(:%(Neg(Succ(Succ(Succ(ww4000000)))), Neg(Succ(ww40100))), ww41)) → new_insertBy051(ww4000000, ww40100, ww3100, ww41, new_primPlusNat0(new_primPlusNat0(new_primPlusNat0(new_primMulNat1(ww4000000, ww3100), Succ(ww3100)), Succ(ww3100)), Succ(ww3100)))
new_insertBy(:%(Neg(Zero), Pos(Succ(ww3100))), :(:%(Neg(Succ(Succ(Succ(ww4000000)))), Pos(Zero)), ww41)) → new_insertBy042(ww4000000, ww3100, ww41, new_primPlusNat0(new_primPlusNat0(new_primPlusNat0(new_primMulNat1(ww4000000, ww3100), Succ(ww3100)), Succ(ww3100)), Succ(ww3100)))
new_insertBy(:%(Neg(Zero), Pos(Succ(ww3100))), :(:%(Neg(Succ(Zero)), Pos(Succ(ww40100))), ww41)) → new_insertBy(:%(Neg(Zero), Pos(Succ(ww3100))), ww41)
new_insertBy039(ww40100, ww3100, ww41, Succ(ww2860)) → new_insertBy(:%(Neg(Zero), Pos(Succ(ww3100))), ww41)
new_insertBy(:%(Neg(Zero), Pos(Succ(ww3100))), :(:%(Neg(Succ(Zero)), Neg(Succ(ww40100))), ww41)) → new_insertBy(:%(Neg(Zero), Pos(Succ(ww3100))), ww41)
new_insertBy(:%(Neg(Zero), Pos(Succ(ww3100))), :(:%(Neg(Succ(Succ(Zero))), Pos(Zero)), ww41)) → new_insertBy043(ww3100, ww41, new_primPlusNat0(new_primPlusNat0(Zero, Succ(ww3100)), Succ(ww3100)))
new_insertBy055(ww4000000, ww3100, ww41, Succ(ww3970)) → new_insertBy(:%(Neg(Zero), Pos(Succ(ww3100))), ww41)
new_insertBy(:%(Neg(Zero), Pos(Succ(ww3100))), :(:%(Neg(Succ(Succ(Zero))), Neg(Zero)), ww41)) → new_insertBy056(ww3100, ww41, new_primPlusNat0(new_primPlusNat0(Zero, Succ(ww3100)), Succ(ww3100)))
new_insertBy056(ww3100, ww41, Succ(ww4010)) → new_insertBy(:%(Neg(Zero), Pos(Succ(ww3100))), ww41)
new_insertBy(:%(Neg(Zero), Pos(Succ(ww3100))), :(:%(Neg(Succ(Succ(Succ(ww4000000)))), Neg(Zero)), ww41)) → new_insertBy055(ww4000000, ww3100, ww41, new_primPlusNat0(new_primPlusNat0(new_primPlusNat0(new_primMulNat1(ww4000000, ww3100), Succ(ww3100)), Succ(ww3100)), Succ(ww3100)))
new_insertBy052(ww40100, ww3100, ww41, Succ(ww3770)) → new_insertBy(:%(Neg(Zero), Pos(Succ(ww3100))), ww41)
new_insertBy043(ww3100, ww41, Succ(ww3100)) → new_insertBy(:%(Neg(Zero), Pos(Succ(ww3100))), ww41)
new_insertBy042(ww4000000, ww3100, ww41, Succ(ww3060)) → new_insertBy(:%(Neg(Zero), Pos(Succ(ww3100))), ww41)
new_insertBy(:%(Neg(Zero), Pos(Succ(ww3100))), :(:%(Neg(Succ(Zero)), Neg(Zero)), ww41)) → new_insertBy(:%(Neg(Zero), Pos(Succ(ww3100))), ww41)
The TRS R consists of the following rules:
new_primPlusNat1(Zero, ww40100) → Succ(ww40100)
new_primPlusNat0(Zero, Zero) → Zero
new_primMulNat1(Zero, ww40100) → Zero
new_primPlusNat1(Succ(ww590), ww40100) → Succ(Succ(new_primPlusNat0(ww590, ww40100)))
new_primPlusNat0(Succ(ww5900), Zero) → Succ(ww5900)
new_primPlusNat0(Zero, Succ(ww401000)) → Succ(ww401000)
new_primPlusNat0(Succ(ww5900), Succ(ww401000)) → Succ(Succ(new_primPlusNat0(ww5900, ww401000)))
new_primMulNat1(Succ(ww30000), ww40100) → new_primPlusNat1(new_primMulNat1(ww30000, ww40100), ww40100)
The set Q consists of the following terms:
new_primMulNat1(Succ(x0), x1)
new_primPlusNat0(Zero, Zero)
new_primPlusNat0(Succ(x0), Zero)
new_primPlusNat0(Zero, Succ(x0))
new_primPlusNat1(Zero, x0)
new_primPlusNat0(Succ(x0), Succ(x1))
new_primMulNat1(Zero, x0)
new_primPlusNat1(Succ(x0), x1)
We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem. From the DPs we obtained the following set of size-change graphs:
- new_insertBy043(ww3100, ww41, Succ(ww3100)) → new_insertBy(:%(Neg(Zero), Pos(Succ(ww3100))), ww41)
The graph contains the following edges 2 >= 2
- new_insertBy(:%(Neg(Zero), Pos(Succ(ww3100))), :(:%(Neg(Succ(Succ(Zero))), Pos(Zero)), ww41)) → new_insertBy043(ww3100, ww41, new_primPlusNat0(new_primPlusNat0(Zero, Succ(ww3100)), Succ(ww3100)))
The graph contains the following edges 1 > 1, 2 > 2
- new_insertBy051(ww4000000, ww40100, ww3100, ww41, Succ(ww3730)) → new_insertBy(:%(Neg(Zero), Pos(Succ(ww3100))), ww41)
The graph contains the following edges 4 >= 2
- new_insertBy(:%(Neg(Zero), Pos(Succ(ww3100))), :(:%(Neg(Succ(Succ(Succ(ww4000000)))), Neg(Succ(ww40100))), ww41)) → new_insertBy051(ww4000000, ww40100, ww3100, ww41, new_primPlusNat0(new_primPlusNat0(new_primPlusNat0(new_primMulNat1(ww4000000, ww3100), Succ(ww3100)), Succ(ww3100)), Succ(ww3100)))
The graph contains the following edges 2 > 1, 2 > 2, 1 > 3, 2 > 4
- new_insertBy042(ww4000000, ww3100, ww41, Succ(ww3060)) → new_insertBy(:%(Neg(Zero), Pos(Succ(ww3100))), ww41)
The graph contains the following edges 3 >= 2
- new_insertBy(:%(Neg(Zero), Pos(Succ(ww3100))), :(:%(Neg(Succ(Succ(Succ(ww4000000)))), Pos(Zero)), ww41)) → new_insertBy042(ww4000000, ww3100, ww41, new_primPlusNat0(new_primPlusNat0(new_primPlusNat0(new_primMulNat1(ww4000000, ww3100), Succ(ww3100)), Succ(ww3100)), Succ(ww3100)))
The graph contains the following edges 2 > 1, 1 > 2, 2 > 3
- new_insertBy038(ww4000000, ww40100, ww3100, ww41, Succ(ww2820)) → new_insertBy(:%(Neg(Zero), Pos(Succ(ww3100))), ww41)
The graph contains the following edges 4 >= 2
- new_insertBy(:%(Neg(Zero), Pos(Succ(ww3100))), :(:%(Neg(Succ(Succ(Succ(ww4000000)))), Pos(Succ(ww40100))), ww41)) → new_insertBy038(ww4000000, ww40100, ww3100, ww41, new_primPlusNat0(new_primPlusNat0(new_primPlusNat0(new_primMulNat1(ww4000000, ww3100), Succ(ww3100)), Succ(ww3100)), Succ(ww3100)))
The graph contains the following edges 2 > 1, 2 > 2, 1 > 3, 2 > 4
- new_insertBy039(ww40100, ww3100, ww41, Succ(ww2860)) → new_insertBy(:%(Neg(Zero), Pos(Succ(ww3100))), ww41)
The graph contains the following edges 3 >= 2
- new_insertBy(:%(Neg(Zero), Pos(Succ(ww3100))), :(:%(Neg(Succ(Succ(Zero))), Pos(Succ(ww40100))), ww41)) → new_insertBy039(ww40100, ww3100, ww41, new_primPlusNat0(new_primPlusNat0(Zero, Succ(ww3100)), Succ(ww3100)))
The graph contains the following edges 2 > 1, 1 > 2, 2 > 3
- new_insertBy052(ww40100, ww3100, ww41, Succ(ww3770)) → new_insertBy(:%(Neg(Zero), Pos(Succ(ww3100))), ww41)
The graph contains the following edges 3 >= 2
- new_insertBy(:%(Neg(Zero), Pos(Succ(ww3100))), :(:%(Neg(Succ(Succ(Zero))), Neg(Succ(ww40100))), ww41)) → new_insertBy052(ww40100, ww3100, ww41, new_primPlusNat0(new_primPlusNat0(Zero, Succ(ww3100)), Succ(ww3100)))
The graph contains the following edges 2 > 1, 1 > 2, 2 > 3
- new_insertBy056(ww3100, ww41, Succ(ww4010)) → new_insertBy(:%(Neg(Zero), Pos(Succ(ww3100))), ww41)
The graph contains the following edges 2 >= 2
- new_insertBy055(ww4000000, ww3100, ww41, Succ(ww3970)) → new_insertBy(:%(Neg(Zero), Pos(Succ(ww3100))), ww41)
The graph contains the following edges 3 >= 2
- new_insertBy(:%(Neg(Zero), Pos(Succ(ww3100))), :(:%(Neg(Succ(Succ(Zero))), Neg(Zero)), ww41)) → new_insertBy056(ww3100, ww41, new_primPlusNat0(new_primPlusNat0(Zero, Succ(ww3100)), Succ(ww3100)))
The graph contains the following edges 1 > 1, 2 > 2
- new_insertBy(:%(Neg(Zero), Pos(Succ(ww3100))), :(:%(Neg(Succ(Succ(Succ(ww4000000)))), Neg(Zero)), ww41)) → new_insertBy055(ww4000000, ww3100, ww41, new_primPlusNat0(new_primPlusNat0(new_primPlusNat0(new_primMulNat1(ww4000000, ww3100), Succ(ww3100)), Succ(ww3100)), Succ(ww3100)))
The graph contains the following edges 2 > 1, 1 > 2, 2 > 3
- new_insertBy(:%(Neg(Zero), Pos(Succ(ww3100))), :(:%(Neg(Succ(Zero)), Neg(Succ(ww40100))), ww41)) → new_insertBy(:%(Neg(Zero), Pos(Succ(ww3100))), ww41)
The graph contains the following edges 1 >= 1, 2 > 2
- new_insertBy(:%(Neg(Zero), Pos(Succ(ww3100))), :(:%(Neg(Succ(Zero)), Pos(Zero)), ww41)) → new_insertBy(:%(Neg(Zero), Pos(Succ(ww3100))), ww41)
The graph contains the following edges 1 >= 1, 2 > 2
- new_insertBy(:%(Neg(Zero), Pos(Succ(ww3100))), :(:%(Neg(Succ(Zero)), Pos(Succ(ww40100))), ww41)) → new_insertBy(:%(Neg(Zero), Pos(Succ(ww3100))), ww41)
The graph contains the following edges 1 >= 1, 2 > 2
- new_insertBy(:%(Neg(Zero), Pos(Succ(ww3100))), :(:%(Neg(Succ(Zero)), Neg(Zero)), ww41)) → new_insertBy(:%(Neg(Zero), Pos(Succ(ww3100))), ww41)
The graph contains the following edges 1 >= 1, 2 > 2
↳ HASKELL
↳ CR
↳ HASKELL
↳ BR
↳ HASKELL
↳ COR
↳ HASKELL
↳ Narrow
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDPSizeChangeProof
↳ QDP
↳ QDP
↳ QDP
Q DP problem:
The TRS P consists of the following rules:
new_insertBy061(ww3000, ww31, ww32, ww3300, ww34, Succ(ww18300), Succ(ww14400)) → new_insertBy061(ww3000, ww31, ww32, ww3300, ww34, ww18300, ww14400)
new_insertBy03(ww2400, ww25, ww26, ww2700, ww28, Succ(ww880)) → new_insertBy084(Succ(ww2400), ww25, ww26, Succ(ww2700), ww28)
new_insertBy084(ww240, ww25, ww26, ww270, ww28) → new_insertBy(:%(Pos(Succ(ww26)), Pos(ww270)), ww28)
new_insertBy(:%(Pos(Succ(ww3000)), Pos(Succ(ww3100))), :(:%(Neg(Succ(Zero)), Pos(Zero)), ww41)) → new_insertBy(:%(Pos(Succ(ww3000)), Pos(Succ(ww3100))), ww41)
new_insertBy060(ww3000, ww31, ww32, ww3300, ww34, Succ(ww1790)) → new_insertBy(:%(Pos(Succ(ww32)), Pos(Succ(ww3300))), ww34)
new_insertBy086(ww2400, ww25, ww26, ww2700, ww28) → new_insertBy(:%(Pos(Succ(ww26)), Neg(Succ(ww2700))), ww28)
new_insertBy085(ww2400, ww25, ww26, ww2700, ww28, Succ(ww6000), Zero) → new_insertBy086(ww2400, ww25, ww26, ww2700, ww28)
new_insertBy(:%(Pos(Succ(ww3000)), Neg(Succ(ww3100))), :(:%(Pos(Succ(Zero)), Pos(Zero)), ww41)) → new_insertBy(:%(Pos(Succ(ww3000)), Neg(Succ(ww3100))), ww41)
new_insertBy058(ww3000, ww31, ww32, ww3300, ww34, Succ(Succ(ww18500)), Succ(ww14400)) → new_insertBy063(ww3000, ww31, ww32, ww3300, ww34, ww18500, ww14400)
new_insertBy04(ww2400, ww25, ww26, ww2700, ww28, Succ(ww6000), Zero) → new_insertBy05(ww2400, ww25, ww26, ww2700, ww28)
new_insertBy(:%(Pos(Succ(ww3000)), Pos(Succ(ww3100))), :(:%(Neg(Succ(Zero)), Neg(Zero)), ww41)) → new_insertBy(:%(Pos(Succ(ww3000)), Pos(Succ(ww3100))), ww41)
new_insertBy(:%(Pos(Succ(ww3000)), ww31), :(:%(ww400, Neg(Succ(ww40100))), ww41)) → new_insertBy018(ww400, ww40100, ww3000, ww31, ww41, new_primPlusNat0(new_primMulNat1(ww3000, ww40100), Succ(ww40100)))
new_insertBy(:%(Pos(Succ(ww3000)), Pos(Succ(ww3100))), :(:%(Neg(Succ(Succ(Zero))), Neg(Zero)), ww41)) → new_insertBy022(ww3000, ww3100, ww41, new_primPlusNat0(new_primPlusNat0(Zero, Succ(ww3100)), Succ(ww3100)))
new_insertBy(:%(Pos(Succ(ww3000)), Pos(Succ(ww3100))), :(:%(Neg(Succ(Succ(Zero))), Pos(Zero)), ww41)) → new_insertBy09(ww3000, ww3100, ww41, new_primPlusNat0(new_primPlusNat0(Zero, Succ(ww3100)), Succ(ww3100)))
new_insertBy057(ww3000, ww31, ww32, ww3300, ww34, Succ(Succ(ww18300)), Zero) → new_insertBy062(ww3000, ww31, ww32, ww3300, ww34)
new_insertBy00(ww2400, ww25, ww26, ww2700, ww28, Succ(ww6000), Succ(Succ(ww9200))) → new_insertBy04(ww2400, ww25, ww26, ww2700, ww28, ww6000, ww9200)
new_insertBy(:%(Pos(Succ(ww3000)), Pos(Succ(ww3100))), :(:%(Neg(Succ(Succ(Succ(ww4000000)))), Pos(Zero)), ww41)) → new_insertBy08(ww4000000, ww3000, ww3100, ww41, new_primPlusNat0(new_primPlusNat0(new_primPlusNat0(new_primMulNat1(ww4000000, ww3100), Succ(ww3100)), Succ(ww3100)), Succ(ww3100)))
new_insertBy085(ww2400, ww25, ww26, ww2700, ww28, Succ(ww6000), Succ(ww9400)) → new_insertBy085(ww2400, ww25, ww26, ww2700, ww28, ww6000, ww9400)
new_insertBy05(ww2400, ww25, ww26, ww2700, ww28) → new_insertBy(:%(Pos(Succ(ww26)), Pos(Succ(ww2700))), ww28)
new_insertBy07(ww3000, ww3100, ww41, Succ(ww700)) → new_insertBy(:%(Pos(Succ(ww3000)), Neg(Succ(ww3100))), ww41)
new_insertBy018(Neg(Succ(ww3000)), ww31, ww32, Pos(Succ(ww3300)), ww34, Zero) → new_insertBy060(ww3000, ww31, ww32, ww3300, ww34, new_primPlusNat0(new_primMulNat1(ww3000, ww3300), Succ(ww3300)))
new_insertBy018(Pos(Succ(ww3000)), ww31, ww32, Neg(Succ(ww3300)), ww34, Zero) → new_insertBy059(ww3000, ww31, ww32, ww3300, ww34, new_primPlusNat0(new_primMulNat1(ww3000, ww3300), Succ(ww3300)))
new_insertBy01(ww2400, ww25, ww26, ww2700, ww28, Succ(ww6000), Succ(Succ(ww9400))) → new_insertBy085(ww2400, ww25, ww26, ww2700, ww28, ww6000, ww9400)
new_insertBy058(ww3000, ww31, ww32, ww3300, ww34, Succ(Succ(ww18500)), Zero) → new_insertBy064(ww3000, ww31, ww32, ww3300, ww34)
new_insertBy00(ww2400, ww25, ww26, ww2700, ww28, Succ(ww6000), Succ(Zero)) → new_insertBy05(ww2400, ww25, ww26, ww2700, ww28)
new_insertBy059(ww3000, ww31, ww32, ww3300, ww34, Succ(ww1770)) → new_insertBy(:%(Pos(Succ(ww32)), Neg(Succ(ww3300))), ww34)
new_insertBy(:%(Pos(Succ(ww3000)), Neg(Succ(ww3100))), :(:%(Pos(Succ(Succ(Zero))), Pos(Zero)), ww41)) → new_insertBy07(ww3000, ww3100, ww41, new_primPlusNat0(new_primPlusNat0(Zero, Succ(ww3100)), Succ(ww3100)))
new_insertBy0(Neg(Zero), ww25, ww26, Neg(Zero), ww28, Succ(ww600)) → new_insertBy(:%(Pos(Succ(ww26)), Neg(Zero)), ww28)
new_insertBy0(Neg(ww240), ww25, ww26, Pos(ww270), ww28, Succ(ww600)) → new_insertBy(:%(Pos(Succ(ww26)), Pos(ww270)), ww28)
new_insertBy00(ww2400, ww25, ww26, ww2700, ww28, ww600, Zero) → new_insertBy(:%(Pos(Succ(ww26)), Pos(Succ(ww2700))), ww28)
new_insertBy021(ww4000000, ww3000, ww3100, ww41, Succ(ww1630)) → new_insertBy(:%(Pos(Succ(ww3000)), Pos(Succ(ww3100))), ww41)
new_insertBy01(ww2400, ww25, ww26, ww2700, ww28, Succ(ww6000), Succ(Zero)) → new_insertBy086(ww2400, ww25, ww26, ww2700, ww28)
new_insertBy(:%(Pos(Succ(ww3000)), ww31), :(:%(ww400, Pos(Succ(ww40100))), ww41)) → new_insertBy0(ww400, ww40100, ww3000, ww31, ww41, new_primPlusNat1(new_primMulNat1(ww3000, ww40100), ww40100))
new_insertBy0(Neg(Succ(ww2400)), ww25, ww26, Neg(Zero), ww28, Succ(ww600)) → new_insertBy(:%(Pos(Succ(ww26)), Neg(Zero)), ww28)
new_insertBy(:%(Pos(Succ(ww3000)), Pos(Succ(ww3100))), :(:%(Neg(Succ(Succ(Succ(ww4000000)))), Neg(Zero)), ww41)) → new_insertBy021(ww4000000, ww3000, ww3100, ww41, new_primPlusNat0(new_primPlusNat0(new_primPlusNat0(new_primMulNat1(ww4000000, ww3100), Succ(ww3100)), Succ(ww3100)), Succ(ww3100)))
new_insertBy0(Neg(Succ(ww2400)), ww25, ww26, Neg(Succ(ww2700)), ww28, Succ(ww600)) → new_insertBy01(ww2400, ww25, ww26, ww2700, ww28, ww600, new_primPlusNat0(new_primMulNat1(ww2400, ww2700), Succ(ww2700)))
new_insertBy018(Pos(Succ(ww3000)), ww31, ww32, Neg(Succ(ww3300)), ww34, Succ(ww1440)) → new_insertBy057(ww3000, ww31, ww32, ww3300, ww34, new_primPlusNat0(new_primMulNat1(ww3000, ww3300), Succ(ww3300)), ww1440)
new_insertBy(:%(Pos(Succ(ww3000)), Neg(Succ(ww3100))), :(:%(Pos(Succ(Succ(Zero))), Neg(Zero)), ww41)) → new_insertBy020(ww3000, ww3100, ww41, new_primPlusNat0(new_primPlusNat0(Zero, Succ(ww3100)), Succ(ww3100)))
new_insertBy(:%(Pos(Succ(ww3000)), Neg(Succ(ww3100))), :(:%(Pos(Succ(Zero)), Neg(Zero)), ww41)) → new_insertBy(:%(Pos(Succ(ww3000)), Neg(Succ(ww3100))), ww41)
new_insertBy083(ww240, ww25, ww26, ww270, ww28) → new_insertBy(:%(Pos(Succ(ww26)), Neg(ww270)), ww28)
new_insertBy0(Neg(Zero), ww25, ww26, Neg(Succ(ww2700)), ww28, Succ(ww600)) → new_insertBy(:%(Pos(Succ(ww26)), Neg(Succ(ww2700))), ww28)
new_insertBy064(ww3000, ww31, ww32, ww3300, ww34) → new_insertBy(:%(Pos(Succ(ww32)), Pos(Succ(ww3300))), ww34)
new_insertBy02(ww2400, ww25, ww26, ww2700, ww28, Succ(ww860)) → new_insertBy083(Succ(ww2400), ww25, ww26, Succ(ww2700), ww28)
new_insertBy0(Pos(Succ(ww2400)), ww25, ww26, Pos(Succ(ww2700)), ww28, Succ(ww600)) → new_insertBy00(ww2400, ww25, ww26, ww2700, ww28, ww600, new_primPlusNat0(new_primMulNat1(ww2400, ww2700), Succ(ww2700)))
new_insertBy0(Pos(ww240), ww25, ww26, Neg(ww270), ww28, Succ(ww600)) → new_insertBy(:%(Pos(Succ(ww26)), Neg(ww270)), ww28)
new_insertBy04(ww2400, ww25, ww26, ww2700, ww28, Succ(ww6000), Succ(ww9200)) → new_insertBy04(ww2400, ww25, ww26, ww2700, ww28, ww6000, ww9200)
new_insertBy057(ww3000, ww31, ww32, ww3300, ww34, Succ(Succ(ww18300)), Succ(ww14400)) → new_insertBy061(ww3000, ww31, ww32, ww3300, ww34, ww18300, ww14400)
new_insertBy063(ww3000, ww31, ww32, ww3300, ww34, Succ(ww18500), Zero) → new_insertBy064(ww3000, ww31, ww32, ww3300, ww34)
new_insertBy08(ww4000000, ww3000, ww3100, ww41, Succ(ww720)) → new_insertBy(:%(Pos(Succ(ww3000)), Pos(Succ(ww3100))), ww41)
new_insertBy063(ww3000, ww31, ww32, ww3300, ww34, Succ(ww18500), Succ(ww14400)) → new_insertBy063(ww3000, ww31, ww32, ww3300, ww34, ww18500, ww14400)
new_insertBy(:%(Pos(Succ(ww3000)), Neg(Succ(ww3100))), :(:%(Pos(Succ(Succ(Succ(ww4000000)))), Pos(Zero)), ww41)) → new_insertBy06(ww4000000, ww3000, ww3100, ww41, new_primPlusNat0(new_primPlusNat0(new_primPlusNat0(new_primMulNat1(ww4000000, ww3100), Succ(ww3100)), Succ(ww3100)), Succ(ww3100)))
new_insertBy061(ww3000, ww31, ww32, ww3300, ww34, Succ(ww18300), Zero) → new_insertBy062(ww3000, ww31, ww32, ww3300, ww34)
new_insertBy022(ww3000, ww3100, ww41, Succ(ww1670)) → new_insertBy(:%(Pos(Succ(ww3000)), Pos(Succ(ww3100))), ww41)
new_insertBy0(Pos(Zero), ww25, ww26, Pos(Succ(ww2700)), ww28, Succ(ww600)) → new_insertBy(:%(Pos(Succ(ww26)), Pos(Succ(ww2700))), ww28)
new_insertBy018(Neg(Succ(ww3000)), ww31, ww32, Pos(Succ(ww3300)), ww34, Succ(ww1440)) → new_insertBy058(ww3000, ww31, ww32, ww3300, ww34, new_primPlusNat0(new_primMulNat1(ww3000, ww3300), Succ(ww3300)), ww1440)
new_insertBy06(ww4000000, ww3000, ww3100, ww41, Succ(ww660)) → new_insertBy(:%(Pos(Succ(ww3000)), Neg(Succ(ww3100))), ww41)
new_insertBy01(ww2400, ww25, ww26, ww2700, ww28, ww600, Zero) → new_insertBy(:%(Pos(Succ(ww26)), Neg(Succ(ww2700))), ww28)
new_insertBy062(ww3000, ww31, ww32, ww3300, ww34) → new_insertBy(:%(Pos(Succ(ww32)), Neg(Succ(ww3300))), ww34)
new_insertBy09(ww3000, ww3100, ww41, Succ(ww760)) → new_insertBy(:%(Pos(Succ(ww3000)), Pos(Succ(ww3100))), ww41)
new_insertBy020(ww3000, ww3100, ww41, Succ(ww1610)) → new_insertBy(:%(Pos(Succ(ww3000)), Neg(Succ(ww3100))), ww41)
new_insertBy0(Pos(Succ(ww2400)), ww25, ww26, Neg(Succ(ww2700)), ww28, Zero) → new_insertBy02(ww2400, ww25, ww26, ww2700, ww28, new_primPlusNat0(new_primMulNat1(ww2400, ww2700), Succ(ww2700)))
new_insertBy0(Neg(Succ(ww2400)), ww25, ww26, Pos(Succ(ww2700)), ww28, Zero) → new_insertBy03(ww2400, ww25, ww26, ww2700, ww28, new_primPlusNat0(new_primMulNat1(ww2400, ww2700), Succ(ww2700)))
new_insertBy0(Pos(Zero), ww25, ww26, Pos(Zero), ww28, Succ(ww600)) → new_insertBy(:%(Pos(Succ(ww26)), Pos(Zero)), ww28)
new_insertBy0(Pos(Succ(ww2400)), ww25, ww26, Pos(Zero), ww28, Succ(ww600)) → new_insertBy(:%(Pos(Succ(ww26)), Pos(Zero)), ww28)
new_insertBy019(ww4000000, ww3000, ww3100, ww41, Succ(ww1570)) → new_insertBy(:%(Pos(Succ(ww3000)), Neg(Succ(ww3100))), ww41)
new_insertBy(:%(Pos(Succ(ww3000)), Neg(Succ(ww3100))), :(:%(Pos(Succ(Succ(Succ(ww4000000)))), Neg(Zero)), ww41)) → new_insertBy019(ww4000000, ww3000, ww3100, ww41, new_primPlusNat0(new_primPlusNat0(new_primPlusNat0(new_primMulNat1(ww4000000, ww3100), Succ(ww3100)), Succ(ww3100)), Succ(ww3100)))
The TRS R consists of the following rules:
new_primPlusNat1(Zero, ww40100) → Succ(ww40100)
new_primPlusNat0(Zero, Zero) → Zero
new_primMulNat1(Zero, ww40100) → Zero
new_primPlusNat1(Succ(ww590), ww40100) → Succ(Succ(new_primPlusNat0(ww590, ww40100)))
new_primPlusNat0(Succ(ww5900), Zero) → Succ(ww5900)
new_primPlusNat0(Zero, Succ(ww401000)) → Succ(ww401000)
new_primPlusNat0(Succ(ww5900), Succ(ww401000)) → Succ(Succ(new_primPlusNat0(ww5900, ww401000)))
new_primMulNat1(Succ(ww30000), ww40100) → new_primPlusNat1(new_primMulNat1(ww30000, ww40100), ww40100)
The set Q consists of the following terms:
new_primMulNat1(Succ(x0), x1)
new_primPlusNat0(Zero, Zero)
new_primPlusNat0(Succ(x0), Zero)
new_primPlusNat0(Zero, Succ(x0))
new_primPlusNat1(Zero, x0)
new_primPlusNat0(Succ(x0), Succ(x1))
new_primMulNat1(Zero, x0)
new_primPlusNat1(Succ(x0), x1)
We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem. From the DPs we obtained the following set of size-change graphs:
- new_insertBy06(ww4000000, ww3000, ww3100, ww41, Succ(ww660)) → new_insertBy(:%(Pos(Succ(ww3000)), Neg(Succ(ww3100))), ww41)
The graph contains the following edges 4 >= 2
- new_insertBy(:%(Pos(Succ(ww3000)), Neg(Succ(ww3100))), :(:%(Pos(Succ(Succ(Succ(ww4000000)))), Pos(Zero)), ww41)) → new_insertBy06(ww4000000, ww3000, ww3100, ww41, new_primPlusNat0(new_primPlusNat0(new_primPlusNat0(new_primMulNat1(ww4000000, ww3100), Succ(ww3100)), Succ(ww3100)), Succ(ww3100)))
The graph contains the following edges 2 > 1, 1 > 2, 1 > 3, 2 > 4
- new_insertBy020(ww3000, ww3100, ww41, Succ(ww1610)) → new_insertBy(:%(Pos(Succ(ww3000)), Neg(Succ(ww3100))), ww41)
The graph contains the following edges 3 >= 2
- new_insertBy(:%(Pos(Succ(ww3000)), Neg(Succ(ww3100))), :(:%(Pos(Succ(Succ(Zero))), Neg(Zero)), ww41)) → new_insertBy020(ww3000, ww3100, ww41, new_primPlusNat0(new_primPlusNat0(Zero, Succ(ww3100)), Succ(ww3100)))
The graph contains the following edges 1 > 1, 1 > 2, 2 > 3
- new_insertBy019(ww4000000, ww3000, ww3100, ww41, Succ(ww1570)) → new_insertBy(:%(Pos(Succ(ww3000)), Neg(Succ(ww3100))), ww41)
The graph contains the following edges 4 >= 2
- new_insertBy(:%(Pos(Succ(ww3000)), Neg(Succ(ww3100))), :(:%(Pos(Succ(Succ(Succ(ww4000000)))), Neg(Zero)), ww41)) → new_insertBy019(ww4000000, ww3000, ww3100, ww41, new_primPlusNat0(new_primPlusNat0(new_primPlusNat0(new_primMulNat1(ww4000000, ww3100), Succ(ww3100)), Succ(ww3100)), Succ(ww3100)))
The graph contains the following edges 2 > 1, 1 > 2, 1 > 3, 2 > 4
- new_insertBy(:%(Pos(Succ(ww3000)), ww31), :(:%(ww400, Neg(Succ(ww40100))), ww41)) → new_insertBy018(ww400, ww40100, ww3000, ww31, ww41, new_primPlusNat0(new_primMulNat1(ww3000, ww40100), Succ(ww40100)))
The graph contains the following edges 2 > 1, 2 > 2, 1 > 3, 1 > 4, 2 > 5
- new_insertBy018(Neg(Succ(ww3000)), ww31, ww32, Pos(Succ(ww3300)), ww34, Succ(ww1440)) → new_insertBy058(ww3000, ww31, ww32, ww3300, ww34, new_primPlusNat0(new_primMulNat1(ww3000, ww3300), Succ(ww3300)), ww1440)
The graph contains the following edges 1 > 1, 2 >= 2, 3 >= 3, 4 > 4, 5 >= 5, 6 > 7
- new_insertBy058(ww3000, ww31, ww32, ww3300, ww34, Succ(Succ(ww18500)), Succ(ww14400)) → new_insertBy063(ww3000, ww31, ww32, ww3300, ww34, ww18500, ww14400)
The graph contains the following edges 1 >= 1, 2 >= 2, 3 >= 3, 4 >= 4, 5 >= 5, 6 > 6, 7 > 7
- new_insertBy058(ww3000, ww31, ww32, ww3300, ww34, Succ(Succ(ww18500)), Zero) → new_insertBy064(ww3000, ww31, ww32, ww3300, ww34)
The graph contains the following edges 1 >= 1, 2 >= 2, 3 >= 3, 4 >= 4, 5 >= 5
- new_insertBy063(ww3000, ww31, ww32, ww3300, ww34, Succ(ww18500), Succ(ww14400)) → new_insertBy063(ww3000, ww31, ww32, ww3300, ww34, ww18500, ww14400)
The graph contains the following edges 1 >= 1, 2 >= 2, 3 >= 3, 4 >= 4, 5 >= 5, 6 > 6, 7 > 7
- new_insertBy063(ww3000, ww31, ww32, ww3300, ww34, Succ(ww18500), Zero) → new_insertBy064(ww3000, ww31, ww32, ww3300, ww34)
The graph contains the following edges 1 >= 1, 2 >= 2, 3 >= 3, 4 >= 4, 5 >= 5
- new_insertBy064(ww3000, ww31, ww32, ww3300, ww34) → new_insertBy(:%(Pos(Succ(ww32)), Pos(Succ(ww3300))), ww34)
The graph contains the following edges 5 >= 2
- new_insertBy(:%(Pos(Succ(ww3000)), ww31), :(:%(ww400, Pos(Succ(ww40100))), ww41)) → new_insertBy0(ww400, ww40100, ww3000, ww31, ww41, new_primPlusNat1(new_primMulNat1(ww3000, ww40100), ww40100))
The graph contains the following edges 2 > 1, 2 > 2, 1 > 3, 1 > 4, 2 > 5
- new_insertBy(:%(Pos(Succ(ww3000)), Neg(Succ(ww3100))), :(:%(Pos(Succ(Succ(Zero))), Pos(Zero)), ww41)) → new_insertBy07(ww3000, ww3100, ww41, new_primPlusNat0(new_primPlusNat0(Zero, Succ(ww3100)), Succ(ww3100)))
The graph contains the following edges 1 > 1, 1 > 2, 2 > 3
- new_insertBy022(ww3000, ww3100, ww41, Succ(ww1670)) → new_insertBy(:%(Pos(Succ(ww3000)), Pos(Succ(ww3100))), ww41)
The graph contains the following edges 3 >= 2
- new_insertBy(:%(Pos(Succ(ww3000)), Pos(Succ(ww3100))), :(:%(Neg(Succ(Succ(Zero))), Neg(Zero)), ww41)) → new_insertBy022(ww3000, ww3100, ww41, new_primPlusNat0(new_primPlusNat0(Zero, Succ(ww3100)), Succ(ww3100)))
The graph contains the following edges 1 > 1, 1 > 2, 2 > 3
- new_insertBy021(ww4000000, ww3000, ww3100, ww41, Succ(ww1630)) → new_insertBy(:%(Pos(Succ(ww3000)), Pos(Succ(ww3100))), ww41)
The graph contains the following edges 4 >= 2
- new_insertBy(:%(Pos(Succ(ww3000)), Pos(Succ(ww3100))), :(:%(Neg(Succ(Succ(Succ(ww4000000)))), Neg(Zero)), ww41)) → new_insertBy021(ww4000000, ww3000, ww3100, ww41, new_primPlusNat0(new_primPlusNat0(new_primPlusNat0(new_primMulNat1(ww4000000, ww3100), Succ(ww3100)), Succ(ww3100)), Succ(ww3100)))
The graph contains the following edges 2 > 1, 1 > 2, 1 > 3, 2 > 4
- new_insertBy09(ww3000, ww3100, ww41, Succ(ww760)) → new_insertBy(:%(Pos(Succ(ww3000)), Pos(Succ(ww3100))), ww41)
The graph contains the following edges 3 >= 2
- new_insertBy(:%(Pos(Succ(ww3000)), Pos(Succ(ww3100))), :(:%(Neg(Succ(Succ(Zero))), Pos(Zero)), ww41)) → new_insertBy09(ww3000, ww3100, ww41, new_primPlusNat0(new_primPlusNat0(Zero, Succ(ww3100)), Succ(ww3100)))
The graph contains the following edges 1 > 1, 1 > 2, 2 > 3
- new_insertBy(:%(Pos(Succ(ww3000)), Pos(Succ(ww3100))), :(:%(Neg(Succ(Succ(Succ(ww4000000)))), Pos(Zero)), ww41)) → new_insertBy08(ww4000000, ww3000, ww3100, ww41, new_primPlusNat0(new_primPlusNat0(new_primPlusNat0(new_primMulNat1(ww4000000, ww3100), Succ(ww3100)), Succ(ww3100)), Succ(ww3100)))
The graph contains the following edges 2 > 1, 1 > 2, 1 > 3, 2 > 4
- new_insertBy08(ww4000000, ww3000, ww3100, ww41, Succ(ww720)) → new_insertBy(:%(Pos(Succ(ww3000)), Pos(Succ(ww3100))), ww41)
The graph contains the following edges 4 >= 2
- new_insertBy00(ww2400, ww25, ww26, ww2700, ww28, ww600, Zero) → new_insertBy(:%(Pos(Succ(ww26)), Pos(Succ(ww2700))), ww28)
The graph contains the following edges 5 >= 2
- new_insertBy05(ww2400, ww25, ww26, ww2700, ww28) → new_insertBy(:%(Pos(Succ(ww26)), Pos(Succ(ww2700))), ww28)
The graph contains the following edges 5 >= 2
- new_insertBy0(Pos(Succ(ww2400)), ww25, ww26, Pos(Succ(ww2700)), ww28, Succ(ww600)) → new_insertBy00(ww2400, ww25, ww26, ww2700, ww28, ww600, new_primPlusNat0(new_primMulNat1(ww2400, ww2700), Succ(ww2700)))
The graph contains the following edges 1 > 1, 2 >= 2, 3 >= 3, 4 > 4, 5 >= 5, 6 > 6
- new_insertBy00(ww2400, ww25, ww26, ww2700, ww28, Succ(ww6000), Succ(Zero)) → new_insertBy05(ww2400, ww25, ww26, ww2700, ww28)
The graph contains the following edges 1 >= 1, 2 >= 2, 3 >= 3, 4 >= 4, 5 >= 5
- new_insertBy00(ww2400, ww25, ww26, ww2700, ww28, Succ(ww6000), Succ(Succ(ww9200))) → new_insertBy04(ww2400, ww25, ww26, ww2700, ww28, ww6000, ww9200)
The graph contains the following edges 1 >= 1, 2 >= 2, 3 >= 3, 4 >= 4, 5 >= 5, 6 > 6, 7 > 7
- new_insertBy04(ww2400, ww25, ww26, ww2700, ww28, Succ(ww6000), Zero) → new_insertBy05(ww2400, ww25, ww26, ww2700, ww28)
The graph contains the following edges 1 >= 1, 2 >= 2, 3 >= 3, 4 >= 4, 5 >= 5
- new_insertBy04(ww2400, ww25, ww26, ww2700, ww28, Succ(ww6000), Succ(ww9200)) → new_insertBy04(ww2400, ww25, ww26, ww2700, ww28, ww6000, ww9200)
The graph contains the following edges 1 >= 1, 2 >= 2, 3 >= 3, 4 >= 4, 5 >= 5, 6 > 6, 7 > 7
- new_insertBy03(ww2400, ww25, ww26, ww2700, ww28, Succ(ww880)) → new_insertBy084(Succ(ww2400), ww25, ww26, Succ(ww2700), ww28)
The graph contains the following edges 2 >= 2, 3 >= 3, 5 >= 5
- new_insertBy084(ww240, ww25, ww26, ww270, ww28) → new_insertBy(:%(Pos(Succ(ww26)), Pos(ww270)), ww28)
The graph contains the following edges 5 >= 2
- new_insertBy060(ww3000, ww31, ww32, ww3300, ww34, Succ(ww1790)) → new_insertBy(:%(Pos(Succ(ww32)), Pos(Succ(ww3300))), ww34)
The graph contains the following edges 5 >= 2
- new_insertBy0(Neg(Succ(ww2400)), ww25, ww26, Pos(Succ(ww2700)), ww28, Zero) → new_insertBy03(ww2400, ww25, ww26, ww2700, ww28, new_primPlusNat0(new_primMulNat1(ww2400, ww2700), Succ(ww2700)))
The graph contains the following edges 1 > 1, 2 >= 2, 3 >= 3, 4 > 4, 5 >= 5
- new_insertBy01(ww2400, ww25, ww26, ww2700, ww28, ww600, Zero) → new_insertBy(:%(Pos(Succ(ww26)), Neg(Succ(ww2700))), ww28)
The graph contains the following edges 5 >= 2
- new_insertBy0(Neg(Succ(ww2400)), ww25, ww26, Neg(Succ(ww2700)), ww28, Succ(ww600)) → new_insertBy01(ww2400, ww25, ww26, ww2700, ww28, ww600, new_primPlusNat0(new_primMulNat1(ww2400, ww2700), Succ(ww2700)))
The graph contains the following edges 1 > 1, 2 >= 2, 3 >= 3, 4 > 4, 5 >= 5, 6 > 6
- new_insertBy0(Pos(Succ(ww2400)), ww25, ww26, Neg(Succ(ww2700)), ww28, Zero) → new_insertBy02(ww2400, ww25, ww26, ww2700, ww28, new_primPlusNat0(new_primMulNat1(ww2400, ww2700), Succ(ww2700)))
The graph contains the following edges 1 > 1, 2 >= 2, 3 >= 3, 4 > 4, 5 >= 5
- new_insertBy086(ww2400, ww25, ww26, ww2700, ww28) → new_insertBy(:%(Pos(Succ(ww26)), Neg(Succ(ww2700))), ww28)
The graph contains the following edges 5 >= 2
- new_insertBy01(ww2400, ww25, ww26, ww2700, ww28, Succ(ww6000), Succ(Succ(ww9400))) → new_insertBy085(ww2400, ww25, ww26, ww2700, ww28, ww6000, ww9400)
The graph contains the following edges 1 >= 1, 2 >= 2, 3 >= 3, 4 >= 4, 5 >= 5, 6 > 6, 7 > 7
- new_insertBy01(ww2400, ww25, ww26, ww2700, ww28, Succ(ww6000), Succ(Zero)) → new_insertBy086(ww2400, ww25, ww26, ww2700, ww28)
The graph contains the following edges 1 >= 1, 2 >= 2, 3 >= 3, 4 >= 4, 5 >= 5
- new_insertBy085(ww2400, ww25, ww26, ww2700, ww28, Succ(ww6000), Succ(ww9400)) → new_insertBy085(ww2400, ww25, ww26, ww2700, ww28, ww6000, ww9400)
The graph contains the following edges 1 >= 1, 2 >= 2, 3 >= 3, 4 >= 4, 5 >= 5, 6 > 6, 7 > 7
- new_insertBy085(ww2400, ww25, ww26, ww2700, ww28, Succ(ww6000), Zero) → new_insertBy086(ww2400, ww25, ww26, ww2700, ww28)
The graph contains the following edges 1 >= 1, 2 >= 2, 3 >= 3, 4 >= 4, 5 >= 5
- new_insertBy07(ww3000, ww3100, ww41, Succ(ww700)) → new_insertBy(:%(Pos(Succ(ww3000)), Neg(Succ(ww3100))), ww41)
The graph contains the following edges 3 >= 2
- new_insertBy02(ww2400, ww25, ww26, ww2700, ww28, Succ(ww860)) → new_insertBy083(Succ(ww2400), ww25, ww26, Succ(ww2700), ww28)
The graph contains the following edges 2 >= 2, 3 >= 3, 5 >= 5
- new_insertBy083(ww240, ww25, ww26, ww270, ww28) → new_insertBy(:%(Pos(Succ(ww26)), Neg(ww270)), ww28)
The graph contains the following edges 5 >= 2
- new_insertBy018(Neg(Succ(ww3000)), ww31, ww32, Pos(Succ(ww3300)), ww34, Zero) → new_insertBy060(ww3000, ww31, ww32, ww3300, ww34, new_primPlusNat0(new_primMulNat1(ww3000, ww3300), Succ(ww3300)))
The graph contains the following edges 1 > 1, 2 >= 2, 3 >= 3, 4 > 4, 5 >= 5
- new_insertBy059(ww3000, ww31, ww32, ww3300, ww34, Succ(ww1770)) → new_insertBy(:%(Pos(Succ(ww32)), Neg(Succ(ww3300))), ww34)
The graph contains the following edges 5 >= 2
- new_insertBy062(ww3000, ww31, ww32, ww3300, ww34) → new_insertBy(:%(Pos(Succ(ww32)), Neg(Succ(ww3300))), ww34)
The graph contains the following edges 5 >= 2
- new_insertBy018(Pos(Succ(ww3000)), ww31, ww32, Neg(Succ(ww3300)), ww34, Zero) → new_insertBy059(ww3000, ww31, ww32, ww3300, ww34, new_primPlusNat0(new_primMulNat1(ww3000, ww3300), Succ(ww3300)))
The graph contains the following edges 1 > 1, 2 >= 2, 3 >= 3, 4 > 4, 5 >= 5
- new_insertBy018(Pos(Succ(ww3000)), ww31, ww32, Neg(Succ(ww3300)), ww34, Succ(ww1440)) → new_insertBy057(ww3000, ww31, ww32, ww3300, ww34, new_primPlusNat0(new_primMulNat1(ww3000, ww3300), Succ(ww3300)), ww1440)
The graph contains the following edges 1 > 1, 2 >= 2, 3 >= 3, 4 > 4, 5 >= 5, 6 > 7
- new_insertBy057(ww3000, ww31, ww32, ww3300, ww34, Succ(Succ(ww18300)), Succ(ww14400)) → new_insertBy061(ww3000, ww31, ww32, ww3300, ww34, ww18300, ww14400)
The graph contains the following edges 1 >= 1, 2 >= 2, 3 >= 3, 4 >= 4, 5 >= 5, 6 > 6, 7 > 7
- new_insertBy057(ww3000, ww31, ww32, ww3300, ww34, Succ(Succ(ww18300)), Zero) → new_insertBy062(ww3000, ww31, ww32, ww3300, ww34)
The graph contains the following edges 1 >= 1, 2 >= 2, 3 >= 3, 4 >= 4, 5 >= 5
- new_insertBy061(ww3000, ww31, ww32, ww3300, ww34, Succ(ww18300), Succ(ww14400)) → new_insertBy061(ww3000, ww31, ww32, ww3300, ww34, ww18300, ww14400)
The graph contains the following edges 1 >= 1, 2 >= 2, 3 >= 3, 4 >= 4, 5 >= 5, 6 > 6, 7 > 7
- new_insertBy061(ww3000, ww31, ww32, ww3300, ww34, Succ(ww18300), Zero) → new_insertBy062(ww3000, ww31, ww32, ww3300, ww34)
The graph contains the following edges 1 >= 1, 2 >= 2, 3 >= 3, 4 >= 4, 5 >= 5
- new_insertBy(:%(Pos(Succ(ww3000)), Neg(Succ(ww3100))), :(:%(Pos(Succ(Zero)), Pos(Zero)), ww41)) → new_insertBy(:%(Pos(Succ(ww3000)), Neg(Succ(ww3100))), ww41)
The graph contains the following edges 1 >= 1, 2 > 2
- new_insertBy(:%(Pos(Succ(ww3000)), Neg(Succ(ww3100))), :(:%(Pos(Succ(Zero)), Neg(Zero)), ww41)) → new_insertBy(:%(Pos(Succ(ww3000)), Neg(Succ(ww3100))), ww41)
The graph contains the following edges 1 >= 1, 2 > 2
- new_insertBy0(Pos(ww240), ww25, ww26, Neg(ww270), ww28, Succ(ww600)) → new_insertBy(:%(Pos(Succ(ww26)), Neg(ww270)), ww28)
The graph contains the following edges 5 >= 2
- new_insertBy0(Neg(Zero), ww25, ww26, Neg(Succ(ww2700)), ww28, Succ(ww600)) → new_insertBy(:%(Pos(Succ(ww26)), Neg(Succ(ww2700))), ww28)
The graph contains the following edges 5 >= 2
- new_insertBy(:%(Pos(Succ(ww3000)), Pos(Succ(ww3100))), :(:%(Neg(Succ(Zero)), Pos(Zero)), ww41)) → new_insertBy(:%(Pos(Succ(ww3000)), Pos(Succ(ww3100))), ww41)
The graph contains the following edges 1 >= 1, 2 > 2
- new_insertBy(:%(Pos(Succ(ww3000)), Pos(Succ(ww3100))), :(:%(Neg(Succ(Zero)), Neg(Zero)), ww41)) → new_insertBy(:%(Pos(Succ(ww3000)), Pos(Succ(ww3100))), ww41)
The graph contains the following edges 1 >= 1, 2 > 2
- new_insertBy0(Neg(ww240), ww25, ww26, Pos(ww270), ww28, Succ(ww600)) → new_insertBy(:%(Pos(Succ(ww26)), Pos(ww270)), ww28)
The graph contains the following edges 5 >= 2
- new_insertBy0(Pos(Zero), ww25, ww26, Pos(Succ(ww2700)), ww28, Succ(ww600)) → new_insertBy(:%(Pos(Succ(ww26)), Pos(Succ(ww2700))), ww28)
The graph contains the following edges 5 >= 2
- new_insertBy0(Neg(Zero), ww25, ww26, Neg(Zero), ww28, Succ(ww600)) → new_insertBy(:%(Pos(Succ(ww26)), Neg(Zero)), ww28)
The graph contains the following edges 5 >= 2
- new_insertBy0(Neg(Succ(ww2400)), ww25, ww26, Neg(Zero), ww28, Succ(ww600)) → new_insertBy(:%(Pos(Succ(ww26)), Neg(Zero)), ww28)
The graph contains the following edges 5 >= 2
- new_insertBy0(Pos(Succ(ww2400)), ww25, ww26, Pos(Zero), ww28, Succ(ww600)) → new_insertBy(:%(Pos(Succ(ww26)), Pos(Zero)), ww28)
The graph contains the following edges 5 >= 2
- new_insertBy0(Pos(Zero), ww25, ww26, Pos(Zero), ww28, Succ(ww600)) → new_insertBy(:%(Pos(Succ(ww26)), Pos(Zero)), ww28)
The graph contains the following edges 5 >= 2
↳ HASKELL
↳ CR
↳ HASKELL
↳ BR
↳ HASKELL
↳ COR
↳ HASKELL
↳ Narrow
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDPSizeChangeProof
↳ QDP
↳ QDP
Q DP problem:
The TRS P consists of the following rules:
new_insertBy049(ww4000000, ww40100, ww3100, ww41, Succ(ww3670)) → new_insertBy(:%(Neg(Zero), Neg(Succ(ww3100))), ww41)
new_insertBy(:%(Neg(Zero), Neg(Succ(ww3100))), :(:%(Pos(Succ(Zero)), Neg(Zero)), ww41)) → new_insertBy(:%(Neg(Zero), Neg(Succ(ww3100))), ww41)
new_insertBy(:%(Neg(Zero), Neg(Succ(ww3100))), :(:%(Pos(Succ(Zero)), Neg(Succ(ww40100))), ww41)) → new_insertBy(:%(Neg(Zero), Neg(Succ(ww3100))), ww41)
new_insertBy(:%(Neg(Zero), Neg(Succ(ww3100))), :(:%(Pos(Succ(Succ(Succ(ww4000000)))), Pos(Zero)), ww41)) → new_insertBy040(ww4000000, ww3100, ww41, new_primPlusNat0(new_primPlusNat0(new_primPlusNat0(new_primMulNat1(ww4000000, ww3100), Succ(ww3100)), Succ(ww3100)), Succ(ww3100)))
new_insertBy(:%(Neg(Zero), Neg(Succ(ww3100))), :(:%(Pos(Succ(Succ(Zero))), Neg(Zero)), ww41)) → new_insertBy054(ww3100, ww41, new_primPlusNat0(new_primPlusNat0(Zero, Succ(ww3100)), Succ(ww3100)))
new_insertBy050(ww40100, ww3100, ww41, Succ(ww3710)) → new_insertBy(:%(Neg(Zero), Neg(Succ(ww3100))), ww41)
new_insertBy(:%(Neg(Zero), Neg(Succ(ww3100))), :(:%(Pos(Succ(Succ(Zero))), Pos(Zero)), ww41)) → new_insertBy041(ww3100, ww41, new_primPlusNat0(new_primPlusNat0(Zero, Succ(ww3100)), Succ(ww3100)))
new_insertBy(:%(Neg(Zero), Neg(Succ(ww3100))), :(:%(Pos(Succ(Zero)), Pos(Zero)), ww41)) → new_insertBy(:%(Neg(Zero), Neg(Succ(ww3100))), ww41)
new_insertBy(:%(Neg(Zero), Neg(Succ(ww3100))), :(:%(Pos(Succ(Succ(Succ(ww4000000)))), Neg(Succ(ww40100))), ww41)) → new_insertBy049(ww4000000, ww40100, ww3100, ww41, new_primPlusNat0(new_primPlusNat0(new_primPlusNat0(new_primMulNat1(ww4000000, ww3100), Succ(ww3100)), Succ(ww3100)), Succ(ww3100)))
new_insertBy(:%(Neg(Zero), Neg(Succ(ww3100))), :(:%(Pos(Succ(Zero)), Pos(Succ(ww40100))), ww41)) → new_insertBy(:%(Neg(Zero), Neg(Succ(ww3100))), ww41)
new_insertBy(:%(Neg(Zero), Neg(Succ(ww3100))), :(:%(Pos(Succ(Succ(Succ(ww4000000)))), Pos(Succ(ww40100))), ww41)) → new_insertBy036(ww4000000, ww40100, ww3100, ww41, new_primPlusNat0(new_primPlusNat0(new_primPlusNat0(new_primMulNat1(ww4000000, ww3100), Succ(ww3100)), Succ(ww3100)), Succ(ww3100)))
new_insertBy041(ww3100, ww41, Succ(ww3040)) → new_insertBy(:%(Neg(Zero), Neg(Succ(ww3100))), ww41)
new_insertBy(:%(Neg(Zero), Neg(Succ(ww3100))), :(:%(Pos(Succ(Succ(Zero))), Neg(Succ(ww40100))), ww41)) → new_insertBy050(ww40100, ww3100, ww41, new_primPlusNat0(new_primPlusNat0(Zero, Succ(ww3100)), Succ(ww3100)))
new_insertBy(:%(Neg(Zero), Neg(Succ(ww3100))), :(:%(Pos(Succ(Succ(Succ(ww4000000)))), Neg(Zero)), ww41)) → new_insertBy053(ww4000000, ww3100, ww41, new_primPlusNat0(new_primPlusNat0(new_primPlusNat0(new_primMulNat1(ww4000000, ww3100), Succ(ww3100)), Succ(ww3100)), Succ(ww3100)))
new_insertBy053(ww4000000, ww3100, ww41, Succ(ww3910)) → new_insertBy(:%(Neg(Zero), Neg(Succ(ww3100))), ww41)
new_insertBy036(ww4000000, ww40100, ww3100, ww41, Succ(ww2760)) → new_insertBy(:%(Neg(Zero), Neg(Succ(ww3100))), ww41)
new_insertBy054(ww3100, ww41, Succ(ww3950)) → new_insertBy(:%(Neg(Zero), Neg(Succ(ww3100))), ww41)
new_insertBy037(ww40100, ww3100, ww41, Succ(ww2800)) → new_insertBy(:%(Neg(Zero), Neg(Succ(ww3100))), ww41)
new_insertBy040(ww4000000, ww3100, ww41, Succ(ww3000)) → new_insertBy(:%(Neg(Zero), Neg(Succ(ww3100))), ww41)
new_insertBy(:%(Neg(Zero), Neg(Succ(ww3100))), :(:%(Pos(Succ(Succ(Zero))), Pos(Succ(ww40100))), ww41)) → new_insertBy037(ww40100, ww3100, ww41, new_primPlusNat0(new_primPlusNat0(Zero, Succ(ww3100)), Succ(ww3100)))
The TRS R consists of the following rules:
new_primPlusNat1(Zero, ww40100) → Succ(ww40100)
new_primPlusNat0(Zero, Zero) → Zero
new_primMulNat1(Zero, ww40100) → Zero
new_primPlusNat1(Succ(ww590), ww40100) → Succ(Succ(new_primPlusNat0(ww590, ww40100)))
new_primPlusNat0(Succ(ww5900), Zero) → Succ(ww5900)
new_primPlusNat0(Zero, Succ(ww401000)) → Succ(ww401000)
new_primPlusNat0(Succ(ww5900), Succ(ww401000)) → Succ(Succ(new_primPlusNat0(ww5900, ww401000)))
new_primMulNat1(Succ(ww30000), ww40100) → new_primPlusNat1(new_primMulNat1(ww30000, ww40100), ww40100)
The set Q consists of the following terms:
new_primMulNat1(Succ(x0), x1)
new_primPlusNat0(Zero, Zero)
new_primPlusNat0(Succ(x0), Zero)
new_primPlusNat0(Zero, Succ(x0))
new_primPlusNat1(Zero, x0)
new_primPlusNat0(Succ(x0), Succ(x1))
new_primMulNat1(Zero, x0)
new_primPlusNat1(Succ(x0), x1)
We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem. From the DPs we obtained the following set of size-change graphs:
- new_insertBy037(ww40100, ww3100, ww41, Succ(ww2800)) → new_insertBy(:%(Neg(Zero), Neg(Succ(ww3100))), ww41)
The graph contains the following edges 3 >= 2
- new_insertBy(:%(Neg(Zero), Neg(Succ(ww3100))), :(:%(Pos(Succ(Succ(Zero))), Pos(Succ(ww40100))), ww41)) → new_insertBy037(ww40100, ww3100, ww41, new_primPlusNat0(new_primPlusNat0(Zero, Succ(ww3100)), Succ(ww3100)))
The graph contains the following edges 2 > 1, 1 > 2, 2 > 3
- new_insertBy040(ww4000000, ww3100, ww41, Succ(ww3000)) → new_insertBy(:%(Neg(Zero), Neg(Succ(ww3100))), ww41)
The graph contains the following edges 3 >= 2
- new_insertBy(:%(Neg(Zero), Neg(Succ(ww3100))), :(:%(Pos(Succ(Succ(Succ(ww4000000)))), Pos(Zero)), ww41)) → new_insertBy040(ww4000000, ww3100, ww41, new_primPlusNat0(new_primPlusNat0(new_primPlusNat0(new_primMulNat1(ww4000000, ww3100), Succ(ww3100)), Succ(ww3100)), Succ(ww3100)))
The graph contains the following edges 2 > 1, 1 > 2, 2 > 3
- new_insertBy049(ww4000000, ww40100, ww3100, ww41, Succ(ww3670)) → new_insertBy(:%(Neg(Zero), Neg(Succ(ww3100))), ww41)
The graph contains the following edges 4 >= 2
- new_insertBy(:%(Neg(Zero), Neg(Succ(ww3100))), :(:%(Pos(Succ(Succ(Succ(ww4000000)))), Neg(Succ(ww40100))), ww41)) → new_insertBy049(ww4000000, ww40100, ww3100, ww41, new_primPlusNat0(new_primPlusNat0(new_primPlusNat0(new_primMulNat1(ww4000000, ww3100), Succ(ww3100)), Succ(ww3100)), Succ(ww3100)))
The graph contains the following edges 2 > 1, 2 > 2, 1 > 3, 2 > 4
- new_insertBy036(ww4000000, ww40100, ww3100, ww41, Succ(ww2760)) → new_insertBy(:%(Neg(Zero), Neg(Succ(ww3100))), ww41)
The graph contains the following edges 4 >= 2
- new_insertBy(:%(Neg(Zero), Neg(Succ(ww3100))), :(:%(Pos(Succ(Succ(Succ(ww4000000)))), Pos(Succ(ww40100))), ww41)) → new_insertBy036(ww4000000, ww40100, ww3100, ww41, new_primPlusNat0(new_primPlusNat0(new_primPlusNat0(new_primMulNat1(ww4000000, ww3100), Succ(ww3100)), Succ(ww3100)), Succ(ww3100)))
The graph contains the following edges 2 > 1, 2 > 2, 1 > 3, 2 > 4
- new_insertBy050(ww40100, ww3100, ww41, Succ(ww3710)) → new_insertBy(:%(Neg(Zero), Neg(Succ(ww3100))), ww41)
The graph contains the following edges 3 >= 2
- new_insertBy(:%(Neg(Zero), Neg(Succ(ww3100))), :(:%(Pos(Succ(Succ(Zero))), Neg(Succ(ww40100))), ww41)) → new_insertBy050(ww40100, ww3100, ww41, new_primPlusNat0(new_primPlusNat0(Zero, Succ(ww3100)), Succ(ww3100)))
The graph contains the following edges 2 > 1, 1 > 2, 2 > 3
- new_insertBy053(ww4000000, ww3100, ww41, Succ(ww3910)) → new_insertBy(:%(Neg(Zero), Neg(Succ(ww3100))), ww41)
The graph contains the following edges 3 >= 2
- new_insertBy(:%(Neg(Zero), Neg(Succ(ww3100))), :(:%(Pos(Succ(Succ(Succ(ww4000000)))), Neg(Zero)), ww41)) → new_insertBy053(ww4000000, ww3100, ww41, new_primPlusNat0(new_primPlusNat0(new_primPlusNat0(new_primMulNat1(ww4000000, ww3100), Succ(ww3100)), Succ(ww3100)), Succ(ww3100)))
The graph contains the following edges 2 > 1, 1 > 2, 2 > 3
- new_insertBy041(ww3100, ww41, Succ(ww3040)) → new_insertBy(:%(Neg(Zero), Neg(Succ(ww3100))), ww41)
The graph contains the following edges 2 >= 2
- new_insertBy054(ww3100, ww41, Succ(ww3950)) → new_insertBy(:%(Neg(Zero), Neg(Succ(ww3100))), ww41)
The graph contains the following edges 2 >= 2
- new_insertBy(:%(Neg(Zero), Neg(Succ(ww3100))), :(:%(Pos(Succ(Succ(Zero))), Pos(Zero)), ww41)) → new_insertBy041(ww3100, ww41, new_primPlusNat0(new_primPlusNat0(Zero, Succ(ww3100)), Succ(ww3100)))
The graph contains the following edges 1 > 1, 2 > 2
- new_insertBy(:%(Neg(Zero), Neg(Succ(ww3100))), :(:%(Pos(Succ(Succ(Zero))), Neg(Zero)), ww41)) → new_insertBy054(ww3100, ww41, new_primPlusNat0(new_primPlusNat0(Zero, Succ(ww3100)), Succ(ww3100)))
The graph contains the following edges 1 > 1, 2 > 2
- new_insertBy(:%(Neg(Zero), Neg(Succ(ww3100))), :(:%(Pos(Succ(Zero)), Pos(Zero)), ww41)) → new_insertBy(:%(Neg(Zero), Neg(Succ(ww3100))), ww41)
The graph contains the following edges 1 >= 1, 2 > 2
- new_insertBy(:%(Neg(Zero), Neg(Succ(ww3100))), :(:%(Pos(Succ(Zero)), Pos(Succ(ww40100))), ww41)) → new_insertBy(:%(Neg(Zero), Neg(Succ(ww3100))), ww41)
The graph contains the following edges 1 >= 1, 2 > 2
- new_insertBy(:%(Neg(Zero), Neg(Succ(ww3100))), :(:%(Pos(Succ(Zero)), Neg(Zero)), ww41)) → new_insertBy(:%(Neg(Zero), Neg(Succ(ww3100))), ww41)
The graph contains the following edges 1 >= 1, 2 > 2
- new_insertBy(:%(Neg(Zero), Neg(Succ(ww3100))), :(:%(Pos(Succ(Zero)), Neg(Succ(ww40100))), ww41)) → new_insertBy(:%(Neg(Zero), Neg(Succ(ww3100))), ww41)
The graph contains the following edges 1 >= 1, 2 > 2
↳ HASKELL
↳ CR
↳ HASKELL
↳ BR
↳ HASKELL
↳ COR
↳ HASKELL
↳ Narrow
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDPSizeChangeProof
↳ QDP
Q DP problem:
The TRS P consists of the following rules:
new_insertBy024(ww40100, ww3100, ww41, Succ(ww1910)) → new_insertBy(:%(Pos(Zero), Neg(Succ(ww3100))), ww41)
new_insertBy(:%(Pos(Zero), Neg(Succ(ww3100))), :(:%(Pos(Succ(Zero)), Pos(Zero)), ww41)) → new_insertBy(:%(Pos(Zero), Neg(Succ(ww3100))), ww41)
new_insertBy(:%(Pos(Zero), Neg(Succ(ww3100))), :(:%(Pos(Succ(Zero)), Pos(Succ(ww40100))), ww41)) → new_insertBy(:%(Pos(Zero), Neg(Succ(ww3100))), ww41)
new_insertBy(:%(Pos(Zero), Neg(Succ(ww3100))), :(:%(Pos(Succ(Succ(Zero))), Pos(Succ(ww40100))), ww41)) → new_insertBy011(ww40100, ww3100, ww41, new_primPlusNat0(new_primPlusNat0(Zero, Succ(ww3100)), Succ(ww3100)))
new_insertBy011(ww40100, ww3100, ww41, Succ(ww1060)) → new_insertBy(:%(Pos(Zero), Neg(Succ(ww3100))), ww41)
new_insertBy027(ww4000000, ww3100, ww41, Succ(ww2110)) → new_insertBy(:%(Pos(Zero), Neg(Succ(ww3100))), ww41)
new_insertBy(:%(Pos(Zero), Neg(Succ(ww3100))), :(:%(Pos(Succ(Succ(Zero))), Neg(Zero)), ww41)) → new_insertBy028(ww3100, ww41, new_primPlusNat0(new_primPlusNat0(Zero, Succ(ww3100)), Succ(ww3100)))
new_insertBy028(ww3100, ww41, Succ(ww2150)) → new_insertBy(:%(Pos(Zero), Neg(Succ(ww3100))), ww41)
new_insertBy(:%(Pos(Zero), Neg(Succ(ww3100))), :(:%(Pos(Succ(Zero)), Neg(Zero)), ww41)) → new_insertBy(:%(Pos(Zero), Neg(Succ(ww3100))), ww41)
new_insertBy014(ww4000000, ww3100, ww41, Succ(ww1260)) → new_insertBy(:%(Pos(Zero), Neg(Succ(ww3100))), ww41)
new_insertBy(:%(Pos(Zero), Neg(Succ(ww3100))), :(:%(Pos(Succ(Zero)), Neg(Succ(ww40100))), ww41)) → new_insertBy(:%(Pos(Zero), Neg(Succ(ww3100))), ww41)
new_insertBy(:%(Pos(Zero), Neg(Succ(ww3100))), :(:%(Pos(Succ(Succ(Zero))), Pos(Zero)), ww41)) → new_insertBy015(ww3100, ww41, new_primPlusNat0(new_primPlusNat0(Zero, Succ(ww3100)), Succ(ww3100)))
new_insertBy(:%(Pos(Zero), Neg(Succ(ww3100))), :(:%(Pos(Succ(Succ(Zero))), Neg(Succ(ww40100))), ww41)) → new_insertBy024(ww40100, ww3100, ww41, new_primPlusNat0(new_primPlusNat0(Zero, Succ(ww3100)), Succ(ww3100)))
new_insertBy(:%(Pos(Zero), Neg(Succ(ww3100))), :(:%(Pos(Succ(Succ(Succ(ww4000000)))), Pos(Succ(ww40100))), ww41)) → new_insertBy010(ww4000000, ww40100, ww3100, ww41, new_primPlusNat0(new_primPlusNat0(new_primPlusNat0(new_primMulNat1(ww4000000, ww3100), Succ(ww3100)), Succ(ww3100)), Succ(ww3100)))
new_insertBy(:%(Pos(Zero), Neg(Succ(ww3100))), :(:%(Pos(Succ(Succ(Succ(ww4000000)))), Neg(Zero)), ww41)) → new_insertBy027(ww4000000, ww3100, ww41, new_primPlusNat0(new_primPlusNat0(new_primPlusNat0(new_primMulNat1(ww4000000, ww3100), Succ(ww3100)), Succ(ww3100)), Succ(ww3100)))
new_insertBy(:%(Pos(Zero), Neg(Succ(ww3100))), :(:%(Pos(Succ(Succ(Succ(ww4000000)))), Pos(Zero)), ww41)) → new_insertBy014(ww4000000, ww3100, ww41, new_primPlusNat0(new_primPlusNat0(new_primPlusNat0(new_primMulNat1(ww4000000, ww3100), Succ(ww3100)), Succ(ww3100)), Succ(ww3100)))
new_insertBy015(ww3100, ww41, Succ(ww1300)) → new_insertBy(:%(Pos(Zero), Neg(Succ(ww3100))), ww41)
new_insertBy(:%(Pos(Zero), Neg(Succ(ww3100))), :(:%(Pos(Succ(Succ(Succ(ww4000000)))), Neg(Succ(ww40100))), ww41)) → new_insertBy023(ww4000000, ww40100, ww3100, ww41, new_primPlusNat0(new_primPlusNat0(new_primPlusNat0(new_primMulNat1(ww4000000, ww3100), Succ(ww3100)), Succ(ww3100)), Succ(ww3100)))
new_insertBy010(ww4000000, ww40100, ww3100, ww41, Succ(ww1020)) → new_insertBy(:%(Pos(Zero), Neg(Succ(ww3100))), ww41)
new_insertBy023(ww4000000, ww40100, ww3100, ww41, Succ(ww1870)) → new_insertBy(:%(Pos(Zero), Neg(Succ(ww3100))), ww41)
The TRS R consists of the following rules:
new_primPlusNat1(Zero, ww40100) → Succ(ww40100)
new_primPlusNat0(Zero, Zero) → Zero
new_primMulNat1(Zero, ww40100) → Zero
new_primPlusNat1(Succ(ww590), ww40100) → Succ(Succ(new_primPlusNat0(ww590, ww40100)))
new_primPlusNat0(Succ(ww5900), Zero) → Succ(ww5900)
new_primPlusNat0(Zero, Succ(ww401000)) → Succ(ww401000)
new_primPlusNat0(Succ(ww5900), Succ(ww401000)) → Succ(Succ(new_primPlusNat0(ww5900, ww401000)))
new_primMulNat1(Succ(ww30000), ww40100) → new_primPlusNat1(new_primMulNat1(ww30000, ww40100), ww40100)
The set Q consists of the following terms:
new_primMulNat1(Succ(x0), x1)
new_primPlusNat0(Zero, Zero)
new_primPlusNat0(Succ(x0), Zero)
new_primPlusNat0(Zero, Succ(x0))
new_primPlusNat1(Zero, x0)
new_primPlusNat0(Succ(x0), Succ(x1))
new_primMulNat1(Zero, x0)
new_primPlusNat1(Succ(x0), x1)
We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem. From the DPs we obtained the following set of size-change graphs:
- new_insertBy(:%(Pos(Zero), Neg(Succ(ww3100))), :(:%(Pos(Succ(Succ(Zero))), Neg(Zero)), ww41)) → new_insertBy028(ww3100, ww41, new_primPlusNat0(new_primPlusNat0(Zero, Succ(ww3100)), Succ(ww3100)))
The graph contains the following edges 1 > 1, 2 > 2
- new_insertBy028(ww3100, ww41, Succ(ww2150)) → new_insertBy(:%(Pos(Zero), Neg(Succ(ww3100))), ww41)
The graph contains the following edges 2 >= 2
- new_insertBy014(ww4000000, ww3100, ww41, Succ(ww1260)) → new_insertBy(:%(Pos(Zero), Neg(Succ(ww3100))), ww41)
The graph contains the following edges 3 >= 2
- new_insertBy(:%(Pos(Zero), Neg(Succ(ww3100))), :(:%(Pos(Succ(Succ(Succ(ww4000000)))), Pos(Zero)), ww41)) → new_insertBy014(ww4000000, ww3100, ww41, new_primPlusNat0(new_primPlusNat0(new_primPlusNat0(new_primMulNat1(ww4000000, ww3100), Succ(ww3100)), Succ(ww3100)), Succ(ww3100)))
The graph contains the following edges 2 > 1, 1 > 2, 2 > 3
- new_insertBy027(ww4000000, ww3100, ww41, Succ(ww2110)) → new_insertBy(:%(Pos(Zero), Neg(Succ(ww3100))), ww41)
The graph contains the following edges 3 >= 2
- new_insertBy(:%(Pos(Zero), Neg(Succ(ww3100))), :(:%(Pos(Succ(Succ(Succ(ww4000000)))), Neg(Zero)), ww41)) → new_insertBy027(ww4000000, ww3100, ww41, new_primPlusNat0(new_primPlusNat0(new_primPlusNat0(new_primMulNat1(ww4000000, ww3100), Succ(ww3100)), Succ(ww3100)), Succ(ww3100)))
The graph contains the following edges 2 > 1, 1 > 2, 2 > 3
- new_insertBy023(ww4000000, ww40100, ww3100, ww41, Succ(ww1870)) → new_insertBy(:%(Pos(Zero), Neg(Succ(ww3100))), ww41)
The graph contains the following edges 4 >= 2
- new_insertBy(:%(Pos(Zero), Neg(Succ(ww3100))), :(:%(Pos(Succ(Succ(Succ(ww4000000)))), Neg(Succ(ww40100))), ww41)) → new_insertBy023(ww4000000, ww40100, ww3100, ww41, new_primPlusNat0(new_primPlusNat0(new_primPlusNat0(new_primMulNat1(ww4000000, ww3100), Succ(ww3100)), Succ(ww3100)), Succ(ww3100)))
The graph contains the following edges 2 > 1, 2 > 2, 1 > 3, 2 > 4
- new_insertBy024(ww40100, ww3100, ww41, Succ(ww1910)) → new_insertBy(:%(Pos(Zero), Neg(Succ(ww3100))), ww41)
The graph contains the following edges 3 >= 2
- new_insertBy(:%(Pos(Zero), Neg(Succ(ww3100))), :(:%(Pos(Succ(Succ(Zero))), Neg(Succ(ww40100))), ww41)) → new_insertBy024(ww40100, ww3100, ww41, new_primPlusNat0(new_primPlusNat0(Zero, Succ(ww3100)), Succ(ww3100)))
The graph contains the following edges 2 > 1, 1 > 2, 2 > 3
- new_insertBy015(ww3100, ww41, Succ(ww1300)) → new_insertBy(:%(Pos(Zero), Neg(Succ(ww3100))), ww41)
The graph contains the following edges 2 >= 2
- new_insertBy(:%(Pos(Zero), Neg(Succ(ww3100))), :(:%(Pos(Succ(Succ(Zero))), Pos(Zero)), ww41)) → new_insertBy015(ww3100, ww41, new_primPlusNat0(new_primPlusNat0(Zero, Succ(ww3100)), Succ(ww3100)))
The graph contains the following edges 1 > 1, 2 > 2
- new_insertBy011(ww40100, ww3100, ww41, Succ(ww1060)) → new_insertBy(:%(Pos(Zero), Neg(Succ(ww3100))), ww41)
The graph contains the following edges 3 >= 2
- new_insertBy010(ww4000000, ww40100, ww3100, ww41, Succ(ww1020)) → new_insertBy(:%(Pos(Zero), Neg(Succ(ww3100))), ww41)
The graph contains the following edges 4 >= 2
- new_insertBy(:%(Pos(Zero), Neg(Succ(ww3100))), :(:%(Pos(Succ(Succ(Zero))), Pos(Succ(ww40100))), ww41)) → new_insertBy011(ww40100, ww3100, ww41, new_primPlusNat0(new_primPlusNat0(Zero, Succ(ww3100)), Succ(ww3100)))
The graph contains the following edges 2 > 1, 1 > 2, 2 > 3
- new_insertBy(:%(Pos(Zero), Neg(Succ(ww3100))), :(:%(Pos(Succ(Succ(Succ(ww4000000)))), Pos(Succ(ww40100))), ww41)) → new_insertBy010(ww4000000, ww40100, ww3100, ww41, new_primPlusNat0(new_primPlusNat0(new_primPlusNat0(new_primMulNat1(ww4000000, ww3100), Succ(ww3100)), Succ(ww3100)), Succ(ww3100)))
The graph contains the following edges 2 > 1, 2 > 2, 1 > 3, 2 > 4
- new_insertBy(:%(Pos(Zero), Neg(Succ(ww3100))), :(:%(Pos(Succ(Zero)), Pos(Succ(ww40100))), ww41)) → new_insertBy(:%(Pos(Zero), Neg(Succ(ww3100))), ww41)
The graph contains the following edges 1 >= 1, 2 > 2
- new_insertBy(:%(Pos(Zero), Neg(Succ(ww3100))), :(:%(Pos(Succ(Zero)), Neg(Zero)), ww41)) → new_insertBy(:%(Pos(Zero), Neg(Succ(ww3100))), ww41)
The graph contains the following edges 1 >= 1, 2 > 2
- new_insertBy(:%(Pos(Zero), Neg(Succ(ww3100))), :(:%(Pos(Succ(Zero)), Neg(Succ(ww40100))), ww41)) → new_insertBy(:%(Pos(Zero), Neg(Succ(ww3100))), ww41)
The graph contains the following edges 1 >= 1, 2 > 2
- new_insertBy(:%(Pos(Zero), Neg(Succ(ww3100))), :(:%(Pos(Succ(Zero)), Pos(Zero)), ww41)) → new_insertBy(:%(Pos(Zero), Neg(Succ(ww3100))), ww41)
The graph contains the following edges 1 >= 1, 2 > 2
↳ HASKELL
↳ CR
↳ HASKELL
↳ BR
↳ HASKELL
↳ COR
↳ HASKELL
↳ Narrow
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDPSizeChangeProof
Q DP problem:
The TRS P consists of the following rules:
new_insertBy(:%(Neg(Succ(ww3000)), Neg(Succ(ww3100))), :(:%(Pos(Succ(Succ(Succ(ww4000000)))), Pos(Zero)), ww41)) → new_insertBy032(ww4000000, ww3000, ww3100, ww41, new_primPlusNat0(new_primPlusNat0(new_primPlusNat0(new_primMulNat1(ww4000000, ww3100), Succ(ww3100)), Succ(ww3100)), Succ(ww3100)))
new_insertBy067(ww4300, ww44, ww45, ww4600, ww47, Succ(ww2600)) → new_insertBy(:%(Neg(Succ(ww45)), Neg(Succ(ww4600))), ww47)
new_insertBy(:%(Neg(Succ(ww3000)), Neg(Succ(ww3100))), :(:%(Pos(Succ(Zero)), Neg(Zero)), ww41)) → new_insertBy(:%(Neg(Succ(ww3000)), Neg(Succ(ww3100))), ww41)
new_insertBy044(Pos(Zero), ww50, ww51, Pos(Succ(ww5200)), ww53, Succ(ww3180)) → new_insertBy(:%(Neg(Succ(ww51)), Pos(Succ(ww5200))), ww53)
new_insertBy073(ww4900, ww50, ww51, ww5200, ww53, Succ(ww31800), Succ(Succ(ww35700))) → new_insertBy077(ww4900, ww50, ww51, ww5200, ww53, ww31800, ww35700)
new_insertBy(:%(Neg(Succ(ww3000)), Neg(Succ(ww3100))), :(:%(Pos(Succ(Zero)), Pos(Zero)), ww41)) → new_insertBy(:%(Neg(Succ(ww3000)), Neg(Succ(ww3100))), ww41)
new_insertBy031(Pos(Succ(ww4300)), ww44, ww45, Neg(Succ(ww4600)), ww47, Succ(ww2290)) → new_insertBy065(ww4300, ww44, ww45, ww4600, ww47, new_primPlusNat0(new_primMulNat1(ww4300, ww4600), Succ(ww4600)), ww2290)
new_insertBy072(ww4300, ww44, ww45, ww4600, ww47) → new_insertBy(:%(Neg(Succ(ww45)), Pos(Succ(ww4600))), ww47)
new_insertBy034(ww4000000, ww3000, ww3100, ww41, Succ(ww2460)) → new_insertBy(:%(Neg(Succ(ww3000)), Pos(Succ(ww3100))), ww41)
new_insertBy077(ww4900, ww50, ww51, ww5200, ww53, Succ(ww31800), Succ(ww35700)) → new_insertBy077(ww4900, ww50, ww51, ww5200, ww53, ww31800, ww35700)
new_insertBy044(Neg(Zero), ww50, ww51, Neg(Succ(ww5200)), ww53, Succ(ww3180)) → new_insertBy(:%(Neg(Succ(ww51)), Neg(Succ(ww5200))), ww53)
new_insertBy073(ww4900, ww50, ww51, ww5200, ww53, Succ(ww31800), Succ(Zero)) → new_insertBy078(ww4900, ww50, ww51, ww5200, ww53)
new_insertBy(:%(Neg(Succ(ww3000)), Neg(Succ(ww3100))), :(:%(Pos(Succ(Succ(Succ(ww4000000)))), Neg(Zero)), ww41)) → new_insertBy045(ww4000000, ww3000, ww3100, ww41, new_primPlusNat0(new_primPlusNat0(new_primPlusNat0(new_primMulNat1(ww4000000, ww3100), Succ(ww3100)), Succ(ww3100)), Succ(ww3100)))
new_insertBy044(Neg(Succ(ww4900)), ww50, ww51, Pos(Succ(ww5200)), ww53, Zero) → new_insertBy076(ww4900, ww50, ww51, ww5200, ww53, new_primPlusNat0(new_primMulNat1(ww4900, ww5200), Succ(ww5200)))
new_insertBy079(ww490, ww50, ww51, ww520, ww53) → new_insertBy(:%(Neg(Succ(ww51)), Neg(ww520)), ww53)
new_insertBy048(ww3000, ww3100, ww41, Succ(ww3410)) → new_insertBy(:%(Neg(Succ(ww3000)), Pos(Succ(ww3100))), ww41)
new_insertBy071(ww4300, ww44, ww45, ww4600, ww47, Succ(ww26800), Zero) → new_insertBy072(ww4300, ww44, ww45, ww4600, ww47)
new_insertBy044(Neg(Succ(ww4900)), ww50, ww51, Neg(Zero), ww53, Succ(ww3180)) → new_insertBy(:%(Neg(Succ(ww51)), Neg(Zero)), ww53)
new_insertBy074(ww4900, ww50, ww51, ww5200, ww53, Succ(ww31800), Succ(Zero)) → new_insertBy082(ww4900, ww50, ww51, ww5200, ww53)
new_insertBy074(ww4900, ww50, ww51, ww5200, ww53, Succ(ww31800), Succ(Succ(ww35900))) → new_insertBy081(ww4900, ww50, ww51, ww5200, ww53, ww31800, ww35900)
new_insertBy033(ww3000, ww3100, ww41, Succ(ww2440)) → new_insertBy(:%(Neg(Succ(ww3000)), Neg(Succ(ww3100))), ww41)
new_insertBy068(ww4300, ww44, ww45, ww4600, ww47, Succ(ww2620)) → new_insertBy(:%(Neg(Succ(ww45)), Pos(Succ(ww4600))), ww47)
new_insertBy(:%(Neg(Succ(ww3000)), Pos(Succ(ww3100))), :(:%(Neg(Succ(Succ(Zero))), Pos(Zero)), ww41)) → new_insertBy035(ww3000, ww3100, ww41, new_primPlusNat0(new_primPlusNat0(Zero, Succ(ww3100)), Succ(ww3100)))
new_insertBy044(Neg(ww490), ww50, ww51, Pos(ww520), ww53, Succ(ww3180)) → new_insertBy(:%(Neg(Succ(ww51)), Pos(ww520)), ww53)
new_insertBy046(ww3000, ww3100, ww41, Succ(ww3350)) → new_insertBy(:%(Neg(Succ(ww3000)), Neg(Succ(ww3100))), ww41)
new_insertBy032(ww4000000, ww3000, ww3100, ww41, Succ(ww2400)) → new_insertBy(:%(Neg(Succ(ww3000)), Neg(Succ(ww3100))), ww41)
new_insertBy(:%(Neg(Succ(ww3000)), Neg(Succ(ww3100))), :(:%(Pos(Succ(Succ(Zero))), Pos(Zero)), ww41)) → new_insertBy033(ww3000, ww3100, ww41, new_primPlusNat0(new_primPlusNat0(Zero, Succ(ww3100)), Succ(ww3100)))
new_insertBy076(ww4900, ww50, ww51, ww5200, ww53, Succ(ww3530)) → new_insertBy080(Succ(ww4900), ww50, ww51, Succ(ww5200), ww53)
new_insertBy(:%(Neg(Succ(ww3000)), ww31), :(:%(ww400, Pos(Succ(ww40100))), ww41)) → new_insertBy031(ww400, ww40100, ww3000, ww31, ww41, new_primPlusNat0(new_primMulNat1(ww3000, ww40100), Succ(ww40100)))
new_insertBy069(ww4300, ww44, ww45, ww4600, ww47, Succ(ww26600), Succ(ww22900)) → new_insertBy069(ww4300, ww44, ww45, ww4600, ww47, ww26600, ww22900)
new_insertBy081(ww4900, ww50, ww51, ww5200, ww53, Succ(ww31800), Zero) → new_insertBy082(ww4900, ww50, ww51, ww5200, ww53)
new_insertBy078(ww4900, ww50, ww51, ww5200, ww53) → new_insertBy(:%(Neg(Succ(ww51)), Pos(Succ(ww5200))), ww53)
new_insertBy074(ww4900, ww50, ww51, ww5200, ww53, ww3180, Zero) → new_insertBy(:%(Neg(Succ(ww51)), Neg(Succ(ww5200))), ww53)
new_insertBy075(ww4900, ww50, ww51, ww5200, ww53, Succ(ww3510)) → new_insertBy079(Succ(ww4900), ww50, ww51, Succ(ww5200), ww53)
new_insertBy(:%(Neg(Succ(ww3000)), Pos(Succ(ww3100))), :(:%(Neg(Succ(Succ(Succ(ww4000000)))), Neg(Zero)), ww41)) → new_insertBy047(ww4000000, ww3000, ww3100, ww41, new_primPlusNat0(new_primPlusNat0(new_primPlusNat0(new_primMulNat1(ww4000000, ww3100), Succ(ww3100)), Succ(ww3100)), Succ(ww3100)))
new_insertBy(:%(Neg(Succ(ww3000)), ww31), :(:%(ww400, Neg(Succ(ww40100))), ww41)) → new_insertBy044(ww400, ww40100, ww3000, ww31, ww41, new_primPlusNat0(new_primMulNat1(ww3000, ww40100), Succ(ww40100)))
new_insertBy044(Pos(Zero), ww50, ww51, Pos(Zero), ww53, Succ(ww3180)) → new_insertBy(:%(Neg(Succ(ww51)), Pos(Zero)), ww53)
new_insertBy047(ww4000000, ww3000, ww3100, ww41, Succ(ww3370)) → new_insertBy(:%(Neg(Succ(ww3000)), Pos(Succ(ww3100))), ww41)
new_insertBy070(ww4300, ww44, ww45, ww4600, ww47) → new_insertBy(:%(Neg(Succ(ww45)), Neg(Succ(ww4600))), ww47)
new_insertBy(:%(Neg(Succ(ww3000)), Pos(Succ(ww3100))), :(:%(Neg(Succ(Zero)), Neg(Zero)), ww41)) → new_insertBy(:%(Neg(Succ(ww3000)), Pos(Succ(ww3100))), ww41)
new_insertBy044(Pos(Succ(ww4900)), ww50, ww51, Pos(Zero), ww53, Succ(ww3180)) → new_insertBy(:%(Neg(Succ(ww51)), Pos(Zero)), ww53)
new_insertBy071(ww4300, ww44, ww45, ww4600, ww47, Succ(ww26800), Succ(ww22900)) → new_insertBy071(ww4300, ww44, ww45, ww4600, ww47, ww26800, ww22900)
new_insertBy(:%(Neg(Succ(ww3000)), Pos(Succ(ww3100))), :(:%(Neg(Succ(Zero)), Pos(Zero)), ww41)) → new_insertBy(:%(Neg(Succ(ww3000)), Pos(Succ(ww3100))), ww41)
new_insertBy069(ww4300, ww44, ww45, ww4600, ww47, Succ(ww26600), Zero) → new_insertBy070(ww4300, ww44, ww45, ww4600, ww47)
new_insertBy066(ww4300, ww44, ww45, ww4600, ww47, Succ(Succ(ww26800)), Zero) → new_insertBy072(ww4300, ww44, ww45, ww4600, ww47)
new_insertBy031(Neg(Succ(ww4300)), ww44, ww45, Pos(Succ(ww4600)), ww47, Succ(ww2290)) → new_insertBy066(ww4300, ww44, ww45, ww4600, ww47, new_primPlusNat0(new_primMulNat1(ww4300, ww4600), Succ(ww4600)), ww2290)
new_insertBy044(Neg(Succ(ww4900)), ww50, ww51, Neg(Succ(ww5200)), ww53, Succ(ww3180)) → new_insertBy074(ww4900, ww50, ww51, ww5200, ww53, ww3180, new_primPlusNat0(new_primMulNat1(ww4900, ww5200), Succ(ww5200)))
new_insertBy031(Pos(Succ(ww4300)), ww44, ww45, Neg(Succ(ww4600)), ww47, Zero) → new_insertBy067(ww4300, ww44, ww45, ww4600, ww47, new_primPlusNat0(new_primMulNat1(ww4300, ww4600), Succ(ww4600)))
new_insertBy065(ww4300, ww44, ww45, ww4600, ww47, Succ(Succ(ww26600)), Zero) → new_insertBy070(ww4300, ww44, ww45, ww4600, ww47)
new_insertBy(:%(Neg(Succ(ww3000)), Pos(Succ(ww3100))), :(:%(Neg(Succ(Succ(Zero))), Neg(Zero)), ww41)) → new_insertBy048(ww3000, ww3100, ww41, new_primPlusNat0(new_primPlusNat0(Zero, Succ(ww3100)), Succ(ww3100)))
new_insertBy045(ww4000000, ww3000, ww3100, ww41, Succ(ww3310)) → new_insertBy(:%(Neg(Succ(ww3000)), Neg(Succ(ww3100))), ww41)
new_insertBy044(Pos(Succ(ww4900)), ww50, ww51, Neg(Succ(ww5200)), ww53, Zero) → new_insertBy075(ww4900, ww50, ww51, ww5200, ww53, new_primPlusNat0(new_primMulNat1(ww4900, ww5200), Succ(ww5200)))
new_insertBy044(Pos(ww490), ww50, ww51, Neg(ww520), ww53, Succ(ww3180)) → new_insertBy(:%(Neg(Succ(ww51)), Neg(ww520)), ww53)
new_insertBy044(Pos(Succ(ww4900)), ww50, ww51, Pos(Succ(ww5200)), ww53, Succ(ww3180)) → new_insertBy073(ww4900, ww50, ww51, ww5200, ww53, ww3180, new_primPlusNat0(new_primMulNat1(ww4900, ww5200), Succ(ww5200)))
new_insertBy066(ww4300, ww44, ww45, ww4600, ww47, Succ(Succ(ww26800)), Succ(ww22900)) → new_insertBy071(ww4300, ww44, ww45, ww4600, ww47, ww26800, ww22900)
new_insertBy035(ww3000, ww3100, ww41, Succ(ww2500)) → new_insertBy(:%(Neg(Succ(ww3000)), Pos(Succ(ww3100))), ww41)
new_insertBy(:%(Neg(Succ(ww3000)), Pos(Succ(ww3100))), :(:%(Neg(Succ(Succ(Succ(ww4000000)))), Pos(Zero)), ww41)) → new_insertBy034(ww4000000, ww3000, ww3100, ww41, new_primPlusNat0(new_primPlusNat0(new_primPlusNat0(new_primMulNat1(ww4000000, ww3100), Succ(ww3100)), Succ(ww3100)), Succ(ww3100)))
new_insertBy(:%(Neg(Succ(ww3000)), Neg(Succ(ww3100))), :(:%(Pos(Succ(Succ(Zero))), Neg(Zero)), ww41)) → new_insertBy046(ww3000, ww3100, ww41, new_primPlusNat0(new_primPlusNat0(Zero, Succ(ww3100)), Succ(ww3100)))
new_insertBy080(ww490, ww50, ww51, ww520, ww53) → new_insertBy(:%(Neg(Succ(ww51)), Pos(ww520)), ww53)
new_insertBy082(ww4900, ww50, ww51, ww5200, ww53) → new_insertBy(:%(Neg(Succ(ww51)), Neg(Succ(ww5200))), ww53)
new_insertBy065(ww4300, ww44, ww45, ww4600, ww47, Succ(Succ(ww26600)), Succ(ww22900)) → new_insertBy069(ww4300, ww44, ww45, ww4600, ww47, ww26600, ww22900)
new_insertBy081(ww4900, ww50, ww51, ww5200, ww53, Succ(ww31800), Succ(ww35900)) → new_insertBy081(ww4900, ww50, ww51, ww5200, ww53, ww31800, ww35900)
new_insertBy077(ww4900, ww50, ww51, ww5200, ww53, Succ(ww31800), Zero) → new_insertBy078(ww4900, ww50, ww51, ww5200, ww53)
new_insertBy031(Neg(Succ(ww4300)), ww44, ww45, Pos(Succ(ww4600)), ww47, Zero) → new_insertBy068(ww4300, ww44, ww45, ww4600, ww47, new_primPlusNat0(new_primMulNat1(ww4300, ww4600), Succ(ww4600)))
new_insertBy073(ww4900, ww50, ww51, ww5200, ww53, ww3180, Zero) → new_insertBy(:%(Neg(Succ(ww51)), Pos(Succ(ww5200))), ww53)
new_insertBy044(Neg(Zero), ww50, ww51, Neg(Zero), ww53, Succ(ww3180)) → new_insertBy(:%(Neg(Succ(ww51)), Neg(Zero)), ww53)
The TRS R consists of the following rules:
new_primPlusNat1(Zero, ww40100) → Succ(ww40100)
new_primPlusNat0(Zero, Zero) → Zero
new_primMulNat1(Zero, ww40100) → Zero
new_primPlusNat1(Succ(ww590), ww40100) → Succ(Succ(new_primPlusNat0(ww590, ww40100)))
new_primPlusNat0(Succ(ww5900), Zero) → Succ(ww5900)
new_primPlusNat0(Zero, Succ(ww401000)) → Succ(ww401000)
new_primPlusNat0(Succ(ww5900), Succ(ww401000)) → Succ(Succ(new_primPlusNat0(ww5900, ww401000)))
new_primMulNat1(Succ(ww30000), ww40100) → new_primPlusNat1(new_primMulNat1(ww30000, ww40100), ww40100)
The set Q consists of the following terms:
new_primMulNat1(Succ(x0), x1)
new_primPlusNat0(Zero, Zero)
new_primPlusNat0(Succ(x0), Zero)
new_primPlusNat0(Zero, Succ(x0))
new_primPlusNat1(Zero, x0)
new_primPlusNat0(Succ(x0), Succ(x1))
new_primMulNat1(Zero, x0)
new_primPlusNat1(Succ(x0), x1)
We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem. From the DPs we obtained the following set of size-change graphs:
- new_insertBy045(ww4000000, ww3000, ww3100, ww41, Succ(ww3310)) → new_insertBy(:%(Neg(Succ(ww3000)), Neg(Succ(ww3100))), ww41)
The graph contains the following edges 4 >= 2
- new_insertBy(:%(Neg(Succ(ww3000)), Neg(Succ(ww3100))), :(:%(Pos(Succ(Succ(Succ(ww4000000)))), Neg(Zero)), ww41)) → new_insertBy045(ww4000000, ww3000, ww3100, ww41, new_primPlusNat0(new_primPlusNat0(new_primPlusNat0(new_primMulNat1(ww4000000, ww3100), Succ(ww3100)), Succ(ww3100)), Succ(ww3100)))
The graph contains the following edges 2 > 1, 1 > 2, 1 > 3, 2 > 4
- new_insertBy033(ww3000, ww3100, ww41, Succ(ww2440)) → new_insertBy(:%(Neg(Succ(ww3000)), Neg(Succ(ww3100))), ww41)
The graph contains the following edges 3 >= 2
- new_insertBy(:%(Neg(Succ(ww3000)), Neg(Succ(ww3100))), :(:%(Pos(Succ(Succ(Zero))), Pos(Zero)), ww41)) → new_insertBy033(ww3000, ww3100, ww41, new_primPlusNat0(new_primPlusNat0(Zero, Succ(ww3100)), Succ(ww3100)))
The graph contains the following edges 1 > 1, 1 > 2, 2 > 3
- new_insertBy046(ww3000, ww3100, ww41, Succ(ww3350)) → new_insertBy(:%(Neg(Succ(ww3000)), Neg(Succ(ww3100))), ww41)
The graph contains the following edges 3 >= 2
- new_insertBy(:%(Neg(Succ(ww3000)), Neg(Succ(ww3100))), :(:%(Pos(Succ(Succ(Zero))), Neg(Zero)), ww41)) → new_insertBy046(ww3000, ww3100, ww41, new_primPlusNat0(new_primPlusNat0(Zero, Succ(ww3100)), Succ(ww3100)))
The graph contains the following edges 1 > 1, 1 > 2, 2 > 3
- new_insertBy(:%(Neg(Succ(ww3000)), ww31), :(:%(ww400, Neg(Succ(ww40100))), ww41)) → new_insertBy044(ww400, ww40100, ww3000, ww31, ww41, new_primPlusNat0(new_primMulNat1(ww3000, ww40100), Succ(ww40100)))
The graph contains the following edges 2 > 1, 2 > 2, 1 > 3, 1 > 4, 2 > 5
- new_insertBy076(ww4900, ww50, ww51, ww5200, ww53, Succ(ww3530)) → new_insertBy080(Succ(ww4900), ww50, ww51, Succ(ww5200), ww53)
The graph contains the following edges 2 >= 2, 3 >= 3, 5 >= 5
- new_insertBy044(Neg(Succ(ww4900)), ww50, ww51, Pos(Succ(ww5200)), ww53, Zero) → new_insertBy076(ww4900, ww50, ww51, ww5200, ww53, new_primPlusNat0(new_primMulNat1(ww4900, ww5200), Succ(ww5200)))
The graph contains the following edges 1 > 1, 2 >= 2, 3 >= 3, 4 > 4, 5 >= 5
- new_insertBy080(ww490, ww50, ww51, ww520, ww53) → new_insertBy(:%(Neg(Succ(ww51)), Pos(ww520)), ww53)
The graph contains the following edges 5 >= 2
- new_insertBy(:%(Neg(Succ(ww3000)), ww31), :(:%(ww400, Pos(Succ(ww40100))), ww41)) → new_insertBy031(ww400, ww40100, ww3000, ww31, ww41, new_primPlusNat0(new_primMulNat1(ww3000, ww40100), Succ(ww40100)))
The graph contains the following edges 2 > 1, 2 > 2, 1 > 3, 1 > 4, 2 > 5
- new_insertBy(:%(Neg(Succ(ww3000)), Neg(Succ(ww3100))), :(:%(Pos(Succ(Succ(Succ(ww4000000)))), Pos(Zero)), ww41)) → new_insertBy032(ww4000000, ww3000, ww3100, ww41, new_primPlusNat0(new_primPlusNat0(new_primPlusNat0(new_primMulNat1(ww4000000, ww3100), Succ(ww3100)), Succ(ww3100)), Succ(ww3100)))
The graph contains the following edges 2 > 1, 1 > 2, 1 > 3, 2 > 4
- new_insertBy035(ww3000, ww3100, ww41, Succ(ww2500)) → new_insertBy(:%(Neg(Succ(ww3000)), Pos(Succ(ww3100))), ww41)
The graph contains the following edges 3 >= 2
- new_insertBy(:%(Neg(Succ(ww3000)), Pos(Succ(ww3100))), :(:%(Neg(Succ(Succ(Zero))), Pos(Zero)), ww41)) → new_insertBy035(ww3000, ww3100, ww41, new_primPlusNat0(new_primPlusNat0(Zero, Succ(ww3100)), Succ(ww3100)))
The graph contains the following edges 1 > 1, 1 > 2, 2 > 3
- new_insertBy047(ww4000000, ww3000, ww3100, ww41, Succ(ww3370)) → new_insertBy(:%(Neg(Succ(ww3000)), Pos(Succ(ww3100))), ww41)
The graph contains the following edges 4 >= 2
- new_insertBy(:%(Neg(Succ(ww3000)), Pos(Succ(ww3100))), :(:%(Neg(Succ(Succ(Succ(ww4000000)))), Neg(Zero)), ww41)) → new_insertBy047(ww4000000, ww3000, ww3100, ww41, new_primPlusNat0(new_primPlusNat0(new_primPlusNat0(new_primMulNat1(ww4000000, ww3100), Succ(ww3100)), Succ(ww3100)), Succ(ww3100)))
The graph contains the following edges 2 > 1, 1 > 2, 1 > 3, 2 > 4
- new_insertBy048(ww3000, ww3100, ww41, Succ(ww3410)) → new_insertBy(:%(Neg(Succ(ww3000)), Pos(Succ(ww3100))), ww41)
The graph contains the following edges 3 >= 2
- new_insertBy(:%(Neg(Succ(ww3000)), Pos(Succ(ww3100))), :(:%(Neg(Succ(Succ(Zero))), Neg(Zero)), ww41)) → new_insertBy048(ww3000, ww3100, ww41, new_primPlusNat0(new_primPlusNat0(Zero, Succ(ww3100)), Succ(ww3100)))
The graph contains the following edges 1 > 1, 1 > 2, 2 > 3
- new_insertBy(:%(Neg(Succ(ww3000)), Pos(Succ(ww3100))), :(:%(Neg(Succ(Succ(Succ(ww4000000)))), Pos(Zero)), ww41)) → new_insertBy034(ww4000000, ww3000, ww3100, ww41, new_primPlusNat0(new_primPlusNat0(new_primPlusNat0(new_primMulNat1(ww4000000, ww3100), Succ(ww3100)), Succ(ww3100)), Succ(ww3100)))
The graph contains the following edges 2 > 1, 1 > 2, 1 > 3, 2 > 4
- new_insertBy067(ww4300, ww44, ww45, ww4600, ww47, Succ(ww2600)) → new_insertBy(:%(Neg(Succ(ww45)), Neg(Succ(ww4600))), ww47)
The graph contains the following edges 5 >= 2
- new_insertBy031(Pos(Succ(ww4300)), ww44, ww45, Neg(Succ(ww4600)), ww47, Zero) → new_insertBy067(ww4300, ww44, ww45, ww4600, ww47, new_primPlusNat0(new_primMulNat1(ww4300, ww4600), Succ(ww4600)))
The graph contains the following edges 1 > 1, 2 >= 2, 3 >= 3, 4 > 4, 5 >= 5
- new_insertBy032(ww4000000, ww3000, ww3100, ww41, Succ(ww2400)) → new_insertBy(:%(Neg(Succ(ww3000)), Neg(Succ(ww3100))), ww41)
The graph contains the following edges 4 >= 2
- new_insertBy070(ww4300, ww44, ww45, ww4600, ww47) → new_insertBy(:%(Neg(Succ(ww45)), Neg(Succ(ww4600))), ww47)
The graph contains the following edges 5 >= 2
- new_insertBy031(Pos(Succ(ww4300)), ww44, ww45, Neg(Succ(ww4600)), ww47, Succ(ww2290)) → new_insertBy065(ww4300, ww44, ww45, ww4600, ww47, new_primPlusNat0(new_primMulNat1(ww4300, ww4600), Succ(ww4600)), ww2290)
The graph contains the following edges 1 > 1, 2 >= 2, 3 >= 3, 4 > 4, 5 >= 5, 6 > 7
- new_insertBy065(ww4300, ww44, ww45, ww4600, ww47, Succ(Succ(ww26600)), Zero) → new_insertBy070(ww4300, ww44, ww45, ww4600, ww47)
The graph contains the following edges 1 >= 1, 2 >= 2, 3 >= 3, 4 >= 4, 5 >= 5
- new_insertBy065(ww4300, ww44, ww45, ww4600, ww47, Succ(Succ(ww26600)), Succ(ww22900)) → new_insertBy069(ww4300, ww44, ww45, ww4600, ww47, ww26600, ww22900)
The graph contains the following edges 1 >= 1, 2 >= 2, 3 >= 3, 4 >= 4, 5 >= 5, 6 > 6, 7 > 7
- new_insertBy069(ww4300, ww44, ww45, ww4600, ww47, Succ(ww26600), Zero) → new_insertBy070(ww4300, ww44, ww45, ww4600, ww47)
The graph contains the following edges 1 >= 1, 2 >= 2, 3 >= 3, 4 >= 4, 5 >= 5
- new_insertBy069(ww4300, ww44, ww45, ww4600, ww47, Succ(ww26600), Succ(ww22900)) → new_insertBy069(ww4300, ww44, ww45, ww4600, ww47, ww26600, ww22900)
The graph contains the following edges 1 >= 1, 2 >= 2, 3 >= 3, 4 >= 4, 5 >= 5, 6 > 6, 7 > 7
- new_insertBy072(ww4300, ww44, ww45, ww4600, ww47) → new_insertBy(:%(Neg(Succ(ww45)), Pos(Succ(ww4600))), ww47)
The graph contains the following edges 5 >= 2
- new_insertBy031(Neg(Succ(ww4300)), ww44, ww45, Pos(Succ(ww4600)), ww47, Succ(ww2290)) → new_insertBy066(ww4300, ww44, ww45, ww4600, ww47, new_primPlusNat0(new_primMulNat1(ww4300, ww4600), Succ(ww4600)), ww2290)
The graph contains the following edges 1 > 1, 2 >= 2, 3 >= 3, 4 > 4, 5 >= 5, 6 > 7
- new_insertBy031(Neg(Succ(ww4300)), ww44, ww45, Pos(Succ(ww4600)), ww47, Zero) → new_insertBy068(ww4300, ww44, ww45, ww4600, ww47, new_primPlusNat0(new_primMulNat1(ww4300, ww4600), Succ(ww4600)))
The graph contains the following edges 1 > 1, 2 >= 2, 3 >= 3, 4 > 4, 5 >= 5
- new_insertBy066(ww4300, ww44, ww45, ww4600, ww47, Succ(Succ(ww26800)), Zero) → new_insertBy072(ww4300, ww44, ww45, ww4600, ww47)
The graph contains the following edges 1 >= 1, 2 >= 2, 3 >= 3, 4 >= 4, 5 >= 5
- new_insertBy066(ww4300, ww44, ww45, ww4600, ww47, Succ(Succ(ww26800)), Succ(ww22900)) → new_insertBy071(ww4300, ww44, ww45, ww4600, ww47, ww26800, ww22900)
The graph contains the following edges 1 >= 1, 2 >= 2, 3 >= 3, 4 >= 4, 5 >= 5, 6 > 6, 7 > 7
- new_insertBy071(ww4300, ww44, ww45, ww4600, ww47, Succ(ww26800), Zero) → new_insertBy072(ww4300, ww44, ww45, ww4600, ww47)
The graph contains the following edges 1 >= 1, 2 >= 2, 3 >= 3, 4 >= 4, 5 >= 5
- new_insertBy034(ww4000000, ww3000, ww3100, ww41, Succ(ww2460)) → new_insertBy(:%(Neg(Succ(ww3000)), Pos(Succ(ww3100))), ww41)
The graph contains the following edges 4 >= 2
- new_insertBy071(ww4300, ww44, ww45, ww4600, ww47, Succ(ww26800), Succ(ww22900)) → new_insertBy071(ww4300, ww44, ww45, ww4600, ww47, ww26800, ww22900)
The graph contains the following edges 1 >= 1, 2 >= 2, 3 >= 3, 4 >= 4, 5 >= 5, 6 > 6, 7 > 7
- new_insertBy068(ww4300, ww44, ww45, ww4600, ww47, Succ(ww2620)) → new_insertBy(:%(Neg(Succ(ww45)), Pos(Succ(ww4600))), ww47)
The graph contains the following edges 5 >= 2
- new_insertBy075(ww4900, ww50, ww51, ww5200, ww53, Succ(ww3510)) → new_insertBy079(Succ(ww4900), ww50, ww51, Succ(ww5200), ww53)
The graph contains the following edges 2 >= 2, 3 >= 3, 5 >= 5
- new_insertBy079(ww490, ww50, ww51, ww520, ww53) → new_insertBy(:%(Neg(Succ(ww51)), Neg(ww520)), ww53)
The graph contains the following edges 5 >= 2
- new_insertBy044(Pos(Succ(ww4900)), ww50, ww51, Neg(Succ(ww5200)), ww53, Zero) → new_insertBy075(ww4900, ww50, ww51, ww5200, ww53, new_primPlusNat0(new_primMulNat1(ww4900, ww5200), Succ(ww5200)))
The graph contains the following edges 1 > 1, 2 >= 2, 3 >= 3, 4 > 4, 5 >= 5
- new_insertBy074(ww4900, ww50, ww51, ww5200, ww53, ww3180, Zero) → new_insertBy(:%(Neg(Succ(ww51)), Neg(Succ(ww5200))), ww53)
The graph contains the following edges 5 >= 2
- new_insertBy082(ww4900, ww50, ww51, ww5200, ww53) → new_insertBy(:%(Neg(Succ(ww51)), Neg(Succ(ww5200))), ww53)
The graph contains the following edges 5 >= 2
- new_insertBy044(Neg(Succ(ww4900)), ww50, ww51, Neg(Succ(ww5200)), ww53, Succ(ww3180)) → new_insertBy074(ww4900, ww50, ww51, ww5200, ww53, ww3180, new_primPlusNat0(new_primMulNat1(ww4900, ww5200), Succ(ww5200)))
The graph contains the following edges 1 > 1, 2 >= 2, 3 >= 3, 4 > 4, 5 >= 5, 6 > 6
- new_insertBy044(Pos(Succ(ww4900)), ww50, ww51, Pos(Succ(ww5200)), ww53, Succ(ww3180)) → new_insertBy073(ww4900, ww50, ww51, ww5200, ww53, ww3180, new_primPlusNat0(new_primMulNat1(ww4900, ww5200), Succ(ww5200)))
The graph contains the following edges 1 > 1, 2 >= 2, 3 >= 3, 4 > 4, 5 >= 5, 6 > 6
- new_insertBy074(ww4900, ww50, ww51, ww5200, ww53, Succ(ww31800), Succ(Zero)) → new_insertBy082(ww4900, ww50, ww51, ww5200, ww53)
The graph contains the following edges 1 >= 1, 2 >= 2, 3 >= 3, 4 >= 4, 5 >= 5
- new_insertBy074(ww4900, ww50, ww51, ww5200, ww53, Succ(ww31800), Succ(Succ(ww35900))) → new_insertBy081(ww4900, ww50, ww51, ww5200, ww53, ww31800, ww35900)
The graph contains the following edges 1 >= 1, 2 >= 2, 3 >= 3, 4 >= 4, 5 >= 5, 6 > 6, 7 > 7
- new_insertBy081(ww4900, ww50, ww51, ww5200, ww53, Succ(ww31800), Zero) → new_insertBy082(ww4900, ww50, ww51, ww5200, ww53)
The graph contains the following edges 1 >= 1, 2 >= 2, 3 >= 3, 4 >= 4, 5 >= 5
- new_insertBy081(ww4900, ww50, ww51, ww5200, ww53, Succ(ww31800), Succ(ww35900)) → new_insertBy081(ww4900, ww50, ww51, ww5200, ww53, ww31800, ww35900)
The graph contains the following edges 1 >= 1, 2 >= 2, 3 >= 3, 4 >= 4, 5 >= 5, 6 > 6, 7 > 7
- new_insertBy073(ww4900, ww50, ww51, ww5200, ww53, ww3180, Zero) → new_insertBy(:%(Neg(Succ(ww51)), Pos(Succ(ww5200))), ww53)
The graph contains the following edges 5 >= 2
- new_insertBy078(ww4900, ww50, ww51, ww5200, ww53) → new_insertBy(:%(Neg(Succ(ww51)), Pos(Succ(ww5200))), ww53)
The graph contains the following edges 5 >= 2
- new_insertBy073(ww4900, ww50, ww51, ww5200, ww53, Succ(ww31800), Succ(Zero)) → new_insertBy078(ww4900, ww50, ww51, ww5200, ww53)
The graph contains the following edges 1 >= 1, 2 >= 2, 3 >= 3, 4 >= 4, 5 >= 5
- new_insertBy073(ww4900, ww50, ww51, ww5200, ww53, Succ(ww31800), Succ(Succ(ww35700))) → new_insertBy077(ww4900, ww50, ww51, ww5200, ww53, ww31800, ww35700)
The graph contains the following edges 1 >= 1, 2 >= 2, 3 >= 3, 4 >= 4, 5 >= 5, 6 > 6, 7 > 7
- new_insertBy077(ww4900, ww50, ww51, ww5200, ww53, Succ(ww31800), Zero) → new_insertBy078(ww4900, ww50, ww51, ww5200, ww53)
The graph contains the following edges 1 >= 1, 2 >= 2, 3 >= 3, 4 >= 4, 5 >= 5
- new_insertBy077(ww4900, ww50, ww51, ww5200, ww53, Succ(ww31800), Succ(ww35700)) → new_insertBy077(ww4900, ww50, ww51, ww5200, ww53, ww31800, ww35700)
The graph contains the following edges 1 >= 1, 2 >= 2, 3 >= 3, 4 >= 4, 5 >= 5, 6 > 6, 7 > 7
- new_insertBy(:%(Neg(Succ(ww3000)), Neg(Succ(ww3100))), :(:%(Pos(Succ(Zero)), Neg(Zero)), ww41)) → new_insertBy(:%(Neg(Succ(ww3000)), Neg(Succ(ww3100))), ww41)
The graph contains the following edges 1 >= 1, 2 > 2
- new_insertBy(:%(Neg(Succ(ww3000)), Neg(Succ(ww3100))), :(:%(Pos(Succ(Zero)), Pos(Zero)), ww41)) → new_insertBy(:%(Neg(Succ(ww3000)), Neg(Succ(ww3100))), ww41)
The graph contains the following edges 1 >= 1, 2 > 2
- new_insertBy044(Neg(Zero), ww50, ww51, Neg(Succ(ww5200)), ww53, Succ(ww3180)) → new_insertBy(:%(Neg(Succ(ww51)), Neg(Succ(ww5200))), ww53)
The graph contains the following edges 5 >= 2
- new_insertBy044(Pos(ww490), ww50, ww51, Neg(ww520), ww53, Succ(ww3180)) → new_insertBy(:%(Neg(Succ(ww51)), Neg(ww520)), ww53)
The graph contains the following edges 5 >= 2
- new_insertBy044(Pos(Zero), ww50, ww51, Pos(Succ(ww5200)), ww53, Succ(ww3180)) → new_insertBy(:%(Neg(Succ(ww51)), Pos(Succ(ww5200))), ww53)
The graph contains the following edges 5 >= 2
- new_insertBy044(Neg(ww490), ww50, ww51, Pos(ww520), ww53, Succ(ww3180)) → new_insertBy(:%(Neg(Succ(ww51)), Pos(ww520)), ww53)
The graph contains the following edges 5 >= 2
- new_insertBy044(Pos(Zero), ww50, ww51, Pos(Zero), ww53, Succ(ww3180)) → new_insertBy(:%(Neg(Succ(ww51)), Pos(Zero)), ww53)
The graph contains the following edges 5 >= 2
- new_insertBy044(Neg(Succ(ww4900)), ww50, ww51, Neg(Zero), ww53, Succ(ww3180)) → new_insertBy(:%(Neg(Succ(ww51)), Neg(Zero)), ww53)
The graph contains the following edges 5 >= 2
- new_insertBy044(Pos(Succ(ww4900)), ww50, ww51, Pos(Zero), ww53, Succ(ww3180)) → new_insertBy(:%(Neg(Succ(ww51)), Pos(Zero)), ww53)
The graph contains the following edges 5 >= 2
- new_insertBy044(Neg(Zero), ww50, ww51, Neg(Zero), ww53, Succ(ww3180)) → new_insertBy(:%(Neg(Succ(ww51)), Neg(Zero)), ww53)
The graph contains the following edges 5 >= 2
- new_insertBy(:%(Neg(Succ(ww3000)), Pos(Succ(ww3100))), :(:%(Neg(Succ(Zero)), Neg(Zero)), ww41)) → new_insertBy(:%(Neg(Succ(ww3000)), Pos(Succ(ww3100))), ww41)
The graph contains the following edges 1 >= 1, 2 > 2
- new_insertBy(:%(Neg(Succ(ww3000)), Pos(Succ(ww3100))), :(:%(Neg(Succ(Zero)), Pos(Zero)), ww41)) → new_insertBy(:%(Neg(Succ(ww3000)), Pos(Succ(ww3100))), ww41)
The graph contains the following edges 1 >= 1, 2 > 2